theorem Th67: :: FUNCT_4:67

for a, b, c, d being object st a <> c holds
(a,c) --> (b,d) = {[a,b],[c,d]}