theorem Th16: :: XXREAL_2:16

for X being real-membered non empty set st X is bounded_above holds
sup X in REAL