theorem Th14: :: PRELAMB:14

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