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:25;
assume X \ Y = Bottom L ; :: thesis: X [= Y
hence X [= Y by A1; :: thesis: verum
end;
assume X [= Y ; :: thesis: X \ Y = Bottom L
then X "/\" (Y `) [= (Y `) "/\" Y by LATTICES:9;
then A2: X "/\" (Y `) [= Bottom L by LATTICES:20;
Bottom L [= X \ Y by LATTICES:16;
hence X \ Y = Bottom L by A2; :: thesis: verum