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 in A & b in A ) by G1, G2, XXREAL_1:1;
then reconsider b = b, a = IT as real number ;
pc1: a <> +infty ;

per cases ( ( IT in REAL & b in REAL ) or ( IT in REAL & b = +infty ) or ( IT = -infty & b in REAL ) or ( IT = -infty & b = +infty ) ) by pc1, XXREAL_0:14;

suppose ( IT in REAL & b in REAL ) ; :: thesis: IT = inf A

A = [.IT,b.] by G2;
hence IT = inf A by G1, XXREAL_2:25; :: thesis: verum

end;

suppose ( IT in REAL & b = +infty ) ; :: thesis: IT = inf A

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

end;

suppose SS: ( IT = -infty & b in REAL ) ; :: thesis: IT = inf A

then A = [.-infty ,b.] by G2;
hence IT = inf A by G1, SS, XXREAL_2:25; :: thesis: verum

end;

suppose SS: ( IT = -infty & b = +infty ) ; :: thesis: IT = inf A

thus IT = inf A by SS; :: thesis: verum

end;

end;