[PostScript]
SetBasics (E, C): trait
  % Essential finite-set operators
  introduces
    {}: -> C
    insert: E, C -> C
    __\in __: E, C -> Bool
  asserts
    C generated by {}, insert
    C partitioned by \in
    forall s: C, e, e1, e2: E
      ~(e \in {});
      e1 \in insert(e2, s) == e1 = e2 \/ e1 \in s
  implies
    InsertGenerated ({} for empty)
    forall e, e1, e2: E, s: C
      insert(e, s) \neq {};
      insert(e, insert(e, s)) == insert(e, s);
      insert(e1, insert(e2, s)) ==
        insert(e2, insert(e1, s))
    converts \in
[Table of Contents] [Index]