Quelle  complete_upper_semilattices.pvs

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

complete_upper_semilattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (complete_upper_semilattice?[T])
]: THEORY

BEGIN

  IMPORTING upper_semilattices[T, <=]

  every_set_is_least_bounded_above: JUDGEMENT
    set[T] SUBTYPE_OF (least_bounded_above?(<=))

END complete_upper_semilattices