let A be connected Subset of R^1; :: thesis: for a, b, c being Real st a <= b & b <= c & a in A & c in A holds
b in A
let a, b, c be Real; :: thesis: ( a <= b & b <= c & a in A & c in A implies b in A )
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A ; :: thesis: b in A

per cases ( a = b or b = c or ( a < b & b < c & a in A & c in A ) ) by A1, A2, A3, A4, XXREAL_0:1;

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

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

end;

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

reconsider B = ].-infty,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
assume not b in A ; :: thesis: contradiction
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: contradiction

per cases ( A c= B or A c= C ) by A6, Th52, CONNSP_1:16;

suppose A c= B ; :: thesis: contradiction

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

end;

suppose A c= C ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;