let A be connected Subset of R^1; :: thesis:
let a, b, c be Real; :: thesis:
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A ; :: thesis:

per cases by A1, A2, A3, A4, XXREAL_0:1;

suppose ( a = b or b = c ) ; :: thesis:

hence b in A by A3, A4; :: thesis:

end;

suppose A5: ( a < b & b < c & a in A & c in A ) ; :: thesis:

reconsider B = ].-infty,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
assume not b in A ; :: thesis:
then A c= REAL \ {b} by TOPMETR:17, ZFMISC_1:34;
then A6: A c= ].-infty,b.[ \/ ].b,+infty.[ by XXREAL_1:389;

now :: thesis:

per cases by A6, Th52, CONNSP_1:16;

suppose A c= B ; :: thesis:

hence contradiction by A5, XXREAL_1:233; :: thesis:

end;

suppose A c= C ; :: thesis:

hence contradiction by A5, XXREAL_1:235; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;