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 A1: <*x*> ==>. y ; :: thesis: ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y )
A2: <*z*> ==>. z by Def18;
then A3: <*(x /" z)*> ^ <*z*> ==>. y by A1, Lm4;
<*z*> ^ <*(z \ x)*> ==>. y by A1, A2, Lm7;
hence ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) by A3, Def18; :: thesis: verum