theorem Th23: :: LATTICES:25

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