let s be SynTypes_Calculus; :: thesis: for x, y being type of s st <*> the carrier of s ==>. x holds
( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y )
let x, y be type of s; :: thesis: ( <*> the carrier of s ==>. x implies ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) )
<*y*> ==>. y by Def19;
then A1: ( H₂(s) ^ <*y*> ==>. y & <*y*> ^ H₂(s) ==>. y ) by FINSEQ_1:47;
assume H₂(s) ==>. x ; :: thesis: ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y )
then ( (H₂(s) ^ <*(y /" x)*>) ^ H₂(s) ==>. y & (H₂(s) ^ <*(x \ y)*>) ^ H₂(s) ==>. y ) by A1, Lm6, Lm10;
then ( H₂(s) ^ <*(y /" x)*> ==>. y & <*(x \ y)*> ^ H₂(s) ==>. y ) by FINSEQ_1:47;
hence ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) by Def19; :: thesis: verum