let GX be non empty TopSpace; :: thesis: ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined implies GX is connected )
given a being Point of GX such that A1: for x being Point of GX holds a,x are_joined ; :: thesis: GX is connected

now :: thesis: for x being Point of GX ex F being Subset-Family of GX st
for C being Subset of GX holds
( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )

let x be Point of GX; :: thesis: ex F being Subset-Family of GX st
for C being Subset of GX holds
( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
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: for C being Subset of GX holds
( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
let C be Subset of GX; :: thesis: ( ( C in F implies ( C is connected & x in C ) ) & ( C is connected & x in C implies C in F ) )
thus ( C in F implies ( C is connected & x in C ) ) :: thesis: ( C is connected & x in C implies C in F )

proof

assume C in F ; :: thesis: ( C is connected & x in C )
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: verum

end;

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

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: for x being object st x in [#] GX holds
x in union F

let x be object ; :: thesis: ( x in [#] GX implies x in union F )
assume x in [#] GX ; :: thesis: x in union F
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: verum

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: verum