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