%-------------------------------------------------------------------------
%
%  Subset chains: sets that are totally ordered by the subset relation.
%
%  For PVS version 3.2.  January 14, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[chain], orders[set[T]], sets[set[T]], sets_lemmas[T]
%  orders: chain[set[T], subset?], subset_chain[T]
%
%-------------------------------------------------------------------------
subset_chain[T: TYPE]: THEORY
 BEGIN

  IMPORTING sets_lemmas[T], chain[set[T], subset?]

  C: VAR chain

  subset_chain_min: THEOREM FORALL C, (S: (C)): subset?(Intersection(C), S)

  subset_chain_intersection: THEOREM
    FORALL C: maximal_chain?(C) => member(Intersection(C), C)

 END subset_chain