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

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;

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

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 ) )

then consider F being Subset-Family of GX such that 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_{1}[ 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_{1}[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 )

end;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

( 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

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

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

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

then
[#] GX c= union F
by TARSKI:def 3;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;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

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