theorem Th12: :: PRELAMB:12

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