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