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