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