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