theorem Th13: :: PRELAMB:13

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