theorem Th18: :: PRELAMB:18

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