let A be connected Subset of R^1 ; :: thesis: for a, b, c being real number st a <= b & b <= c & a in A & c in A holds
b in A
let a, b, c be real number ; :: thesis: ( a <= b & b <= c & a in A & c in A implies b in A )
assume A1: ( a <= b & b <= c & a in A & 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, XXREAL_0:1;

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

hence b in A by A1; :: thesis: verum

end;

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

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

now

per cases ( A c= B or A c= C ) by A3, Th79, CONNSP_1:17;

suppose A c= B ; :: thesis: contradiction

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

end;

suppose A c= C ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;