theorem Th57: :: XXREAL_2:57

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