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