[PostScript]
Semilattice (T): trait
  assumes PartialOrder
  includes GreatestLowerBound
  introduces
    \bot: -> T
    __\lub __: T, T -> T
  asserts forall x, y, z: T
    \bot <= x;
    x \lub y == y \lub x;
    x \glb y == y \glb x;
    x <= (x \lub y);
    (x <= z /\ y <= z) => (x \lub y) <= z
  implies 
    AbelianMonoid (\lub for \circ, \bot for unit),
    AbelianSemigroup (\glb for \circ)
[Table of Contents] [Index]