let a, c be Real; :: thesis:
let b be R_eal; :: thesis:
assume that
A1: a < b and
A2: [.a,b.[ c= [.a,c.[ ; :: thesis:
set K = [.a,b.[;
A3: not c in [.a,b.[ by A2, XXREAL_1:3;

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

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

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

suppose c < x ; :: thesis:

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

end;

suppose x <= c ; :: thesis:

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

end;

end;

end;

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

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

end;

end;