let x, y, z be boolean set ; :: thesis: ( x <= y => z iff x '&' y <= z )
thus ( x <= y => z implies x '&' y <= z ) :: thesis: ( x '&' y <= z implies x <= y => z )

proof

assume x <= y => z ; :: thesis: x '&' y <= z
then A1: x => (y => z) = TRUE by Def3;
x => (y => z) = (x '&' y) => z ;
hence x '&' y <= z by A1, Def3; :: thesis: verum

end;

assume x '&' y <= z ; :: thesis: x <= y => z
then A2: (x '&' y) => z = TRUE by Def3;
(x '&' y) => z = x => (y => z) ;
hence x <= y => z by A2, Def3; :: thesis: verum