theorem :: MEASURE6:6

for eps being ExtReal
for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds
ex x being ExtReal st
( x in X & (sup X) - eps < x )