let a, c be Real; :: thesis: for b being R_eal st a < b & [.a,b.[ c= [.a,c.[ holds
b is Real
let b be R_eal; :: thesis: ( a < b & [.a,b.[ c= [.a,c.[ implies b is Real )
assume that
A1: a < b and
A2: [.a,b.[ c= [.a,c.[ ; :: thesis: b is Real
set K = [.a,b.[;
A3: not c in [.a,b.[ by A2, XXREAL_1:3;

per cases ( not [.a,b.[ is empty or [.a,b.[ is empty ) ;

suppose A4: not [.a,b.[ is empty ; :: thesis: b is Real

then consider x being object such that
A5: x in [.a,b.[ ;
reconsider x = x as Real by A5;
assume b is not Real ; :: thesis: contradiction
then ( not b in REAL & a in REAL & a <= b ) by XREAL_0:def 1, A4, XXREAL_1:27;
then A6: b = +infty by XXREAL_0:10;
a <= x by A5, XXREAL_1:3;
then A7: [.x,+infty.[ c= [.a,b.[ by A6, XXREAL_1:38;

per cases ( c < x or x <= c ) ;

suppose c < x ; :: thesis: contradiction

hence contradiction by A5, A2, XXREAL_1:3; :: thesis: verum

end;

suppose x <= c ; :: thesis: contradiction

hence contradiction by A3, A7, XXREAL_1:236; :: thesis: verum

end;

end;

end;

suppose [.a,b.[ is empty ; :: thesis: b is Real

hence b is Real by A1, XXREAL_1:31; :: thesis: verum

end;

end;