theorem :: PRELAMB:25

for s being SynTypes_Calculus
for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x) by Th13, Th18;