let X be set ; :: thesis: for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )
let x, y be Element of (BoolePoset X); :: thesis: ( x <= y iff x c= y )
reconsider x9 = x, y9 = y as Element of (BooleLatt X) ;
thus ( x <= y implies x c= y ) :: thesis: ( x c= y implies x <= y )

proof

assume x <= y ; :: thesis: x c= y
then x9 % <= y9 % ;
then x9 [= y9 by LATTICE3:7;
hence x c= y by LATTICE3:2; :: thesis: verum

end;

assume x c= y ; :: thesis: x <= y
then x9 [= y9 by LATTICE3:2;
then x9 % <= y9 % by LATTICE3:7;
hence x <= y ; :: thesis: verum