theorem Th1: :: XXREAL_2:1

for x, y being ExtReal holds
( y is UpperBound of {x} iff x <= y )