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

proof

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

end;

( x <= y => z implies x '&' y <= z )

proof

assume x <= y => z ; :: thesis: x '&' y <= z
then A3: x => (y => z) = TRUE by BVFUNC_1:def 3;
x => (y => z) = (x '&' y) => z ;
hence x '&' y <= z by A3, BVFUNC_1:def 3; :: thesis: verum

end;

hence ( x <= y => z iff x '&' y <= z ) by A1; :: thesis: verum