let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s holds
( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) )
let x, y, z be type of s; :: thesis: ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) )
A1: <*(x /" y)*> ==>. (x /" z) /" (y /" z) by Th14;
<*(y \ x)*> ==>. (z \ y) \ (z \ x) by Th15;
hence ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) ) by A1, Th19; :: thesis: verum