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