theorem Th21: :: WAYBEL_4:21

for L being non empty lower-bounded Poset
for I being Ideal of L holds Bottom L in I