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 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 A3: A c= [.0 ,1.] \ {b} by BORSUK_1:83, ZFMISC_1:40;
A4: ( 0 <= a & c <= 1 ) by BORSUK_1:86;
then A5: ( 0 < b & b < 1 ) by A2, XXREAL_0:2;
then A6: A c= [.0 ,b.[ \/ ].b,1.] by A3, XXREAL_1:201;
A7: ( [.0 ,b.[ c= [.0 ,b.] & ].b,1.] c= [.b,1.] ) by XXREAL_1:23, XXREAL_1:24;
( b in [.0 ,1.] & 0 in [.0 ,1.] & 1 in [.0 ,1.] ) by A5, XXREAL_1:1;
then ( [.0 ,b.] c= [.0 ,1.] & [.b,1.] c= [.0 ,1.] ) by XXREAL_2:def 12;
then reconsider B = [.0 ,b.[, C = ].b,1.] as non empty Subset of I[01] by A2, A4, A7, BORSUK_1:83, XBOOLE_1:1, XXREAL_1:2, XXREAL_1:3;

now

per cases ( A c= B or A c= C ) by A5, A6, Th33, CONNSP_1:17;

suppose A c= B ; :: thesis: contradiction

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

end;

suppose A c= C ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;