let L be B_Lattice; :: thesis: for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )
let X, Y be Element of L; :: thesis: ( X \ Y = Bottom L iff X [= Y )
thus ( X \ Y = Bottom L implies X [= Y ) :: thesis: ( X [= Y implies X \ Y = Bottom L )

proof

A1: ( X "/\" (Y `) = Bottom L implies X [= (Y `) ` ) by LATTICES:52;
assume X \ Y = Bottom L ; :: thesis: X [= Y
hence X [= Y by A1, LATTICES:49; :: thesis: verum

end;

assume X [= Y ; :: thesis: X \ Y = Bottom L
then X "/\" (Y `) [= (Y `) "/\" Y by LATTICES:27;
then A2: X "/\" (Y `) [= Bottom L by LATTICES:47;
Bottom L [= X \ Y by LATTICES:41;
hence X \ Y = Bottom L by A2, Def3; :: thesis: verum