SSL converse_zorn.pvs   Interaktion und
PortierbarkeitPVS

%-------------------------------------------------------------------------
%
%  The converse of Zorn's lemma: if every chain has a lower bound, then
%  the set has a minimal element.
%
%  For PVS version 3.2.  January 17, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T], relations[T], sets[T]
%  orders: bounded_orders[T], chain[T,<=], converse_zorn[T,<=],
%    minmax_orders[T], relations_extra[T]
%
%-------------------------------------------------------------------------
converse_zorn[T: TYPE, <=: (partial_order?[T])]: THEORY

 EXPORTING ALL WITH orders[T], relations[T], sets[T], bounded_orders[T],
           chain[T, <=], minmax_orders[T], relations_extra[T]

 BEGIN

  IMPORTING minmax_orders[T], chain[T, <=]
  IMPORTING relation_converse_props[T], zorn[T, converse(<=)] % Proof only

  converse_zorn: THEOREM
    (FORALL (ch: chain[T, <=]): bounded_below?[T](ch, <=)) =>
     (EXISTS (t: T): minimal?[T](t, fullset[T], <=))

 END converse_zorn