let GX be non empty TopSpace; :: thesis:
given a being Point of GX such that A1: for x being Point of GX holds a,x are_joined ; :: thesis:

now :: thesis:

let x be Point of GX; :: thesis:
defpred S₁[ set ] means ex C1 being Subset of GX st
( C1 = $1 & C1 is connected & x in $1 );
consider F being Subset-Family of GX such that
A2: for C being Subset of GX holds
( C in F iff S₁[C] ) from SUBSET_1:sch 3();
take F = F; :: thesis:
let C be Subset of GX; :: thesis:
thus ( C in F implies ( C is connected & x in C ) ) :: thesis:

proof

assume C in F ; :: thesis:
then ex C1 being Subset of GX st
( C1 = C & C1 is connected & x in C ) by A2;
hence ( C is connected & x in C ) ; :: thesis:

end;

thus ( C is connected & x in C implies C in F ) by A2; :: thesis:

end;

then consider F being Subset-Family of GX such that
A3: for C being Subset of GX holds
( C in F iff ( C is connected & a in C ) ) ;
A4: for x being Point of GX ex C being Subset of GX st
( C is connected & a in C & x in C ) by A1, Def4;

now :: thesis:

let x be object ; :: thesis:
assume x in [#] GX ; :: thesis:
then consider C being Subset of GX such that
A5: C is connected and
A6: a in C and
A7: x in C by A4;
C in F by A3, A5, A6;
hence x in union F by A7, TARSKI:def 4; :: thesis:

end;

then [#] GX c= union F by TARSKI:def 3;
then A8: union F = [#] GX ;
A9: for A being set st A in F holds
a in A by A3;
a in {a} by TARSKI:def 1;
then F <> {} by A3;
then A10: meet F <> {} GX by A9, SETFAM_1:def 1;
for A being Subset of GX st A in F holds
A is connected by A3;
then [#] GX is connected by A8, A10, Th26;
hence GX is connected by Th27; :: thesis: