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_2:25;