theorem Th15: :: MEASURE6:15

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