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