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 by XXREAL_1:26, XXREAL_2:27;