theorem Th17: :: PRELAMB:17

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