let A be non empty connected Subset of I[01] ; :: thesis: for a, b being real number st a in A & b in A holds
[.a,b.] c= A
let a, b be real number ; :: thesis: ( a in A & b in A implies [.a,b.] c= A )
assume A1: ( a in A & b in A ) ; :: thesis: [.a,b.] c= A
then A2: ( 0 <= a & b <= 1 ) by BORSUK_1:86;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,b.] or x in A )
assume x in [.a,b.] ; :: thesis: 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 & a <= z & z <= b ) ;
( 0 <= z & z <= 1 ) by A2, A3, XXREAL_0:2;
then reconsider z = z as Point of I[01] by BORSUK_1:86;
z in A by A1, A3, Th46;
hence x in A by A3; :: thesis: verum