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

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

suppose ( IT in REAL & a in REAL ) ; :: thesis: IT = sup A

A = [.a,IT.] by G2;
hence IT = sup A by G1, XXREAL_2:29; :: thesis: verum

end;

suppose ( IT in REAL & a = -infty ) ; :: thesis: IT = sup A

then A: A = ].-infty ,IT.] ;
then -infty < IT by XXREAL_1:26;
hence IT = sup A by A, XXREAL_2:30; :: thesis: verum

end;

suppose SS: ( IT = +infty & a in REAL ) ; :: thesis: IT = sup A

then A = [.a,+infty .] by G2;
hence IT = sup A by SS, G1, XXREAL_2:29; :: thesis: verum

end;

suppose SS: ( IT = +infty & a = -infty ) ; :: thesis: IT = sup A

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

end;

end;