% sets ordered by "subset?" form a complete lattice
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Jan 2005

sets_complete_lattices[T: TYPE]: THEORY

BEGIN

  IMPORTING booleans_are_finite, pointwise_orders[T, bool]
  
  subset_equals_pointwise_implies: LEMMA
    subset?[T] = pointwise(IMPLIES)

  subset_is_a_complete_lattice: JUDGEMENT
    subset?[T] HAS_TYPE (complete_lattice?[set[T]])

  IMPORTING complete_lattices[set[T], subset?[T]]

END sets_complete_lattices