theorem :: LATTICES:16

for L being 0_Lattice
for a being Element of L holds Bottom L [= a ;