let A be non empty connected Subset of I[01]; :: thesis: for a, b, c being Point of I[01] st a <= b & b <= c & a in A & c in A holds
b in A
let a, b, c be Point of I[01]; :: 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

A6: ].b,1.] c= [.b,1.] by XXREAL_1:23;
A7: [.0,b.[ c= [.0,b.] by XXREAL_1:24;
A8: 0 <= a by BORSUK_1:43;
A9: c <= 1 by BORSUK_1:43;
then A10: b < 1 by A5, XXREAL_0:2;
then A11: b in [.0,1.] by A5, A8, XXREAL_1:1;
1 in [.0,1.] by XXREAL_1:1;
then A12: [.b,1.] c= [.0,1.] by A11, XXREAL_2:def 12;
0 in [.0,1.] by XXREAL_1:1;
then [.0,b.] c= [.0,1.] by A11, XXREAL_2:def 12;
then reconsider B = [.0,b.[, C = ].b,1.] as non empty Subset of I[01] by A5, A8, A9, A7, A6, A12, BORSUK_1:40, XBOOLE_1:1, XXREAL_1:2, XXREAL_1:3;
assume not b in A ; :: thesis: contradiction
then A c= [.0,1.] \ {b} by BORSUK_1:40, ZFMISC_1:34;
then A13: A c= [.0,b.[ \/ ].b,1.] by A5, A8, A10, XXREAL_1:201;

now :: thesis: contradiction

per cases ( A c= B or A c= C ) by A5, A8, A10, A13, Th14, CONNSP_1:16;

suppose A c= B ; :: thesis: contradiction

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

end;

suppose A c= C ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;