theorem Th58: :: XXREAL_2:58

for X being ext-real-membered non empty set st X is bounded_below & X <> {+infty} holds
inf X in REAL