let A be connected Subset of R^1; :: thesis: for a, b being Real st a in A & b in A holds
[.a,b.] c= A
let a, b be Real; :: thesis: ( a in A & b in A implies [.a,b.] c= A )
assume that
A1: a in A and
A2: b in A ; :: thesis: [.a,b.] c= A
let x be object ; :: 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 ex z being Real st
( z = x & a <= z & z <= b ) ;
hence x in A by A1, A2, Th75; :: thesis: verum