theorem ThMin02: :: POSET_2:1

for P being non empty lower-bounded Poset
for p being Element of P st p is_<=_than the carrier of P holds
p = Bottom P