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