Function RELATION-UNIVERSE

A relation-universe of a relation of any arity is a class from which is drawn every item in every tuple of the relation. Like EXACT-DOMAIN, it is exactly those items and no other. Thus, to state that the universe of a relation is covered by some class, one can state that the relation-universe is a subclass of the covering class.
Arity: 2
Domain: Relation
Range: Class
Axioms:
(<=> (Relation-Universe ?Relation ?Type-Class)
     (And (Relation ?Relation)
          (Class ?Type-Class)
          (Forall (?X)
                  (<=> (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (Item ?X ?Tuple)))
                       (Instance-Of ?X ?Type-Class)))))
Notes: