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