for s being SynTypes_Calculus
for x, y, z being type of s holds
( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) )