let GX be TopSpace; :: thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds

A is connected ) & meet F <> {} GX holds

union F is connected

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in F holds

A is connected ) & meet F <> {} GX implies union F is connected )

assume that

A1: for A being Subset of GX st A in F holds

A is connected and

A2: meet F <> {} GX ; :: thesis: union F is connected

consider x being Point of GX such that

A3: x in meet F by A2, PRE_TOPC:12;

meet F c= union F by SETFAM_1:2;

then consider A2 being set such that

A4: x in A2 and

A5: A2 in F by A3, TARSKI:def 4;

reconsider A2 = A2 as Subset of GX by A5;

hence union F is connected by A1, A5, A6, Th25; :: thesis: verum

A is connected ) & meet F <> {} GX holds

union F is connected

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in F holds

A is connected ) & meet F <> {} GX implies union F is connected )

assume that

A1: for A being Subset of GX st A in F holds

A is connected and

A2: meet F <> {} GX ; :: thesis: union F is connected

consider x being Point of GX such that

A3: x in meet F by A2, PRE_TOPC:12;

meet F c= union F by SETFAM_1:2;

then consider A2 being set such that

A4: x in A2 and

A5: A2 in F by A3, TARSKI:def 4;

reconsider A2 = A2 as Subset of GX by A5;

A6: now :: thesis: for B being Subset of GX st B in F & B <> A2 holds

not A2,B are_separated

A2 <> {} GX
by A4;not A2,B are_separated

let B be Subset of GX; :: thesis: ( B in F & B <> A2 implies not A2,B are_separated )

assume that

A7: B in F and

B <> A2 ; :: thesis: not A2,B are_separated

A2 c= Cl A2 by PRE_TOPC:18;

then ( ( x in Cl A2 & x in B ) or ( x in A2 & x in Cl B ) ) by A3, A4, A7, SETFAM_1:def 1;

then ( (Cl A2) /\ B <> {} or A2 /\ (Cl B) <> {} ) by XBOOLE_0:def 4;

then ( Cl A2 meets B or A2 meets Cl B ) ;

hence not A2,B are_separated ; :: thesis: verum

end;assume that

A7: B in F and

B <> A2 ; :: thesis: not A2,B are_separated

A2 c= Cl A2 by PRE_TOPC:18;

then ( ( x in Cl A2 & x in B ) or ( x in A2 & x in Cl B ) ) by A3, A4, A7, SETFAM_1:def 1;

then ( (Cl A2) /\ B <> {} or A2 /\ (Cl B) <> {} ) by XBOOLE_0:def 4;

then ( Cl A2 meets B or A2 meets Cl B ) ;

hence not A2,B are_separated ; :: thesis: verum

hence union F is connected by A1, A5, A6, Th25; :: thesis: verum