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)
.= (X "\/" Y) "/\" ((Y `) "\/" Y) by LATTICES:21
.= (X \ Y) "\/" Y by LATTICES:11 ; :: thesis: verum