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