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