theorem :: MEASURE6:14

for A being non empty Interval
for b being ExtReal st ex a being ExtReal st
( a <= b & A = [.a,b.] ) holds
b = sup A by XXREAL_2:29;