Quelle  complete_lower_semilattices.pvs

% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004

complete_lower_semilattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (complete_lower_semilattice?[T])
]: THEORY

BEGIN

  IMPORTING lower_semilattices[T, <=]

  every_set_is_greatest_bounded_below: JUDGEMENT
    set[T] SUBTYPE_OF (greatest_bounded_below?(<=))

END complete_lower_semilattices