let A be non empty connected Subset of I[01]; 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]; ( 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
; 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 A5:
(
a < b &
b < c &
a in A &
c in A )
;
b in AA6:
].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
;
contradictionthen
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;
hence
contradiction
;
verum end;