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