for L being B_Lattice
for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y