theorem Th64: :: BOOLEALG:64

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