Function COMPOSITION

The composition of binary relations R_1 and R_2 is a relation R_3 such that R_1(x,y) and R_2(y,z) implies R_3(x,z).
Arity: 3
Axioms:
(Nth-Domain Composition 3 Binary-Relation)

(Nth-Domain Composition 2 Binary-Relation)

(Nth-Domain Composition 1 Binary-Relation)

(=> (Composition ?R1 ?R2 ?R3)
    (And (Binary-Relation ?R1)
         (Binary-Relation ?R2)
         (= ?R3
            (Setofall (Listof ?X ?Z)
                      (Exists (?Y)
                              (And (Holds ?R1 ?X ?Y)
                                   (Holds ?R2 ?Y ?Z)))))))