[PostScript]
SetToRelation: trait
  % Map a (finitely generated) set
  % to the relation that represents it.
  assumes SetBasics, RelationBasics
  introduces
    relation: C -> R
  asserts
    forall e: E, s: C
      relation({}) == \bot;
      relation(insert(e, s)) == [e, e] \U relation(s)
  implies
    forall e: E, s: C
      e \in s == e \langle relation(s) \rangle e
    converts relation
[Table of Contents] [Index]