let L be B_Lattice; :: thesis: for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y
let X, Y be Element of L; :: thesis: X "\/" Y = (X \ Y) "\/" Y
thus X "\/" Y = (X "\/" Y) "/\" (Top L) by LATTICES:43
.= (X "\/" Y) "/\" ((Y ` ) "\/" Y) by LATTICES:48
.= (X \ Y) "\/" Y by LATTICES:31 ; :: thesis: verum