let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s st <*x*> ==>. y holds
( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z )
let x, y, z be type of s; :: thesis: ( <*x*> ==>. y implies ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) )
assume <*x*> ==>. y ; :: thesis: ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z )
then ( <*x*> ==>. y & <*z*> ==>. z ) by Def19;
then ( <*(z /" y)*> ^ <*x*> ==>. z & <*x*> ^ <*(y \ z)*> ==>. z ) by Lm8, Lm11;
hence ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) by Def19; :: thesis: verum