let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x)
let x, y, z be type of s; :: thesis: <*(y \ x)*> ==>. (z \ y) \ (z \ x)
A1: <*y*> ^ <*(y \ x)*> ==>. x by Th12;
<*z*> ==>. z by Def18;
then (<*z*> ^ <*(z \ y)*>) ^ <*(y \ x)*> ==>. x by A1, Lm6;
then <*z*> ^ (<*(z \ y)*> ^ <*(y \ x)*>) ==>. x by FINSEQ_1:32;
then <*(z \ y)*> ^ <*(y \ x)*> ==>. z \ x by Def18;
hence <*(y \ x)*> ==>. (z \ y) \ (z \ x) by Def18; :: thesis: verum