let A be non empty Interval; :: thesis: for a being R_eal st ex b being R_eal st
( a <= b & A = ].a,b.] ) holds
a = inf A
let IT be R_eal; :: thesis: ( ex b being R_eal st
( IT <= b & A = ].IT,b.] ) implies IT = inf A )
given b being R_eal such that G1: IT <= b and
G2: A = ].IT,b.] ; :: thesis: IT = inf A
IT <> b by G2;
then IT < b by G1, XXREAL_0:1;
then b in A by G2, XXREAL_1:2;
then reconsider b = b as real number ;

per cases ( b in REAL or b = +infty ) by XXREAL_0:14;

suppose b in REAL ; :: thesis: IT = inf A

A: A = ].IT,b.] by G2;
then IT < b by XXREAL_1:26;
hence IT = inf A by A, XXREAL_2:27; :: thesis: verum

end;

suppose b = +infty ; :: thesis: IT = inf A

then A: A = ].IT,+infty .[ ;
then IT < +infty by XXREAL_1:28;
hence IT = inf A by A, XXREAL_2:28; :: thesis: verum

end;

end;