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 S1[ 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 S1[C] ) from 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 ;
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 ; :: 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 ;
for A being Subset of GX st A in F holds
A is connected by A3;
then [#] GX is connected by ;
hence GX is connected by Th27; :: thesis: verum