theorem :: PRELAMB:24

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