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