%-------------------------------------------------------------------------
%
%  Kuratowski's lemma: there exists a maximal chain.  This is equivalent
%  to Zorn's lemma and the Axiom of Choice.
%
%  For PVS version 3.2.  January 17, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[chain[T,<=]], orders[T], sets[T]
%  orders: chain[T,<=], kuratowski[T,<=]
%
%-------------------------------------------------------------------------
kuratowski[T: TYPE, <=: (partial_order?[T])]: THEORY

 % Hide the imports used only in the proof
 EXPORTING ALL WITH orders[T], sets[T], orders[chain[T, <=]], chain[T, <=]

 BEGIN

  IMPORTING chain_chain[T, <=], zorn[subchain, chain_incl]

  kuratowski: THEOREM EXISTS (ch: chain[T, <=]): maximal_chain?[T, <=](ch)

 END kuratowski