theorem :: LATTICES:14

for L being 0_Lattice
for a being Element of L holds (Bottom L) "\/" a = a ;