let s be SynTypes_Calculus; :: thesis: for y, x, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x)
let y, x, z be type of s; :: thesis: <*(y \ x)*> ==>. (z \ y) \ (z \ x)
( <*y*> ^ <*(y \ x)*> ==>. x & <*z*> ==>. z ) by Def19, Th12;
then (<*z*> ^ <*(z \ y)*>) ^ <*(y \ x)*> ==>. x by Lm10;
then <*z*> ^ (<*(z \ y)*> ^ <*(y \ x)*>) ==>. x by FINSEQ_1:45;
then <*(z \ y)*> ^ <*(y \ x)*> ==>. z \ x by Def19;
hence <*(y \ x)*> ==>. (z \ y) \ (z \ x) by Def19; :: thesis: verum