theorem :: PRELAMB:16

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