let s be SynTypes_Calculus; :: thesis: for x, y being type of s holds <*(y /" ((y /" x) \ y))*> ==>. y /" x
let x, y be type of s; :: thesis: <*(y /" ((y /" x) \ y))*> ==>. y /" x
<*x*> ==>. (y /" x) \ y by Th13;
hence <*(y /" ((y /" x) \ y))*> ==>. y /" x by Th17; :: thesis: verum