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