let L be B_Lattice; :: thesis: for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)
let X, Y be Element of L; :: thesis: X \+\ Y = (X "\/" Y) \ (X "/\" Y)
thus X \+\ Y = (X \ (X "/\" Y)) "\/" (Y \ X) by Th33
.= (X \ (X "/\" Y)) "\/" (Y \ (X "/\" Y)) by Th33
.= (X "\/" Y) \ (X "/\" Y) by LATTICES:def 11 ; :: thesis: verum