let A be non empty connected Subset of I[01]; for a, b being Real st a in A & b in A holds
[.a,b.] c= A
let a, b be Real; ( a in A & b in A implies [.a,b.] c= A )
assume that
A1:
a in A
and
A2:
b in A
; [.a,b.] c= A
let x be object ; TARSKI:def 3 ( not x in [.a,b.] or x in A )
assume
x in [.a,b.]
; x in A
then
x in { y where y is Real : ( a <= y & y <= b ) }
by RCOMP_1:def 1;
then consider z being Real such that
A3:
z = x
and
A4:
a <= z
and
A5:
z <= b
;
A6:
0 <= z
by A1, A4, BORSUK_1:43;
b <= 1
by A2, BORSUK_1:43;
then
z <= 1
by A5, XXREAL_0:2;
then reconsider z = z as Point of I[01] by A6, BORSUK_1:43;
z in A
by A1, A2, A4, A5, Th18;
hence
x in A
by A3; verum