theorem Th18: :: LATTICES:20

for L being B_Lattice
for a being Element of L holds (a `) "/\" a = Bottom L