theorem Th49: :: XXREAL_2:49

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