theorem :: PRELAMB:28

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