theorem :: BOOLEALG:59
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)