theorem Th50: :: XXREAL_2:50

for X being ext-real-membered non empty bounded_below set st X <> {+infty} holds
ex x being Element of REAL st x in X