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