theorem Th2: :: XXREAL_2:2

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