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