[PostScript]
IsPO (<=, T): trait
  % <<= is a partial order on T
  introduces __<=__: T, T -> Bool
  asserts forall x, y, z: T    
    x <= x;
    (x <= y /\ y <= z) => x <= z;
    x <= y /\ y <= x == x = y
  implies
    Antisymmetric (<=),
    PreOrder,
    Reflexive (<=),
    Transitive (<=)
    T partitioned by <=
[Table of Contents] [Index]