theorem :: LATTICES:15

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