theorem Th23: :: WAYBEL_4:23

for L being non empty lower-bounded Poset holds downarrow (Bottom L) = {(Bottom L)}