The projection of an N-ary relation on column i is the class whose instances are the ith items of each tuple in the relation.
(<=> (Projection ?Relation ?Column)
(And (Defined (Arity ?Relation))
(Positive-Integer ?Column)
(=< ?Column (Arity ?Relation))
(Class ?Projection-Relation)
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column)
?Instance)))))))
(Nth-Domain Projection 3 Class) (Nth-Domain Projection 2 Positive-Integer)
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance))))))
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(Class ?Projection-Relation))
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(=< ?Column (Arity ?Relation)))
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(Positive-Integer ?Column))
(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
(Defined (Arity ?Relation)))