theorem Th15: :: PRELAMB:15

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