theorem :: PRELAMB:21

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