let L be B_Lattice; :: thesis: for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L
let X, Y be Element of L; :: thesis: X \ (X "\/" Y) = Bottom L
X [= X "\/" Y by LATTICES:22;
hence X \ (X "\/" Y) = Bottom L by Th46; :: thesis: verum