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