theorem Th11: :: MEASURE6:11

for A being non empty Interval
for a being ExtReal st ex b being ExtReal st
( a <= b & A = [.a,b.[ ) holds
a = inf A