theorem Th9: :: BOOLEALG:9

for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L by LATTICES:16;