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_1:28, XXREAL_2:32;