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

proof

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

end;

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