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