theorem :: BOOLEALG:27

for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L