% $Id$
ClosedInterval(E, C): trait
  includes
    Set(E, C),
    TotalOrder(E)

  introduces
    min: C -> E
    max: C -> E

  asserts forall x: E, s:C
    x \in s == x <= max(s) /\ x >= min(s)