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 ) )
A1: <*y*> ==>. y by Def18;
then A2: H₂(s) ^ <*y*> ==>. y by FINSEQ_1:34;
A3: <*y*> ^ H₂(s) ==>. y by A1, FINSEQ_1:34;
assume A4: H₂(s) ==>. x ; :: thesis: ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y )
then A5: (H₂(s) ^ <*(y /" x)*>) ^ H₂(s) ==>. y by A2, Lm2;
A6: (H₂(s) ^ <*(x \ y)*>) ^ H₂(s) ==>. y by A3, A4, Lm6;
A7: H₂(s) ^ <*(y /" x)*> ==>. y by A5, FINSEQ_1:34;
<*(x \ y)*> ^ H₂(s) ==>. y by A6, FINSEQ_1:34;
hence ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) by A7, Def18; :: thesis: verum