theorem Th29: :: BOOLEALG:29
for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )