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 ) & ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) 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 ) & ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) implies union F is connected )

assume that

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

A is connected and

A2: ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) ; :: thesis: union F is connected

consider A1 being Subset of GX such that

A1 <> {} GX and

A3: A1 in F and

A4: for B being Subset of GX st B in F & B <> A1 holds

not A1,B are_separated by A2;

reconsider A1 = A1 as Subset of GX ;

A is connected ) & ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) 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 ) & ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) implies union F is connected )

assume that

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

A is connected and

A2: ex A being Subset of GX st

( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds

not A,B are_separated ) ) ; :: thesis: union F is connected

consider A1 being Subset of GX such that

A1 <> {} GX and

A3: A1 in F and

A4: for B being Subset of GX st B in F & B <> A1 holds

not A1,B are_separated by A2;

reconsider A1 = A1 as Subset of GX ;

now :: thesis: for P, Q being Subset of GX st union F = P \/ Q & P,Q are_separated & not P = {} GX holds

Q = {} GX

hence
union F is connected
by Th15; :: thesis: verumQ = {} GX

let P, Q be Subset of GX; :: thesis: ( union F = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )

assume that

A5: union F = P \/ Q and

A6: P,Q are_separated ; :: thesis: ( P = {} GX or Q = {} GX )

P misses Q by A6, Th1;

then A7: P /\ Q = {} ;

hence ( P = {} GX or Q = {} GX ) by A1, A3, A6, A13, A8, Th16; :: thesis: verum

end;assume that

A5: union F = P \/ Q and

A6: P,Q are_separated ; :: thesis: ( P = {} GX or Q = {} GX )

P misses Q by A6, Th1;

then A7: P /\ Q = {} ;

A8: now :: thesis: ( A1 c= Q implies P = {} GX )

assume A9:
A1 c= Q
; :: thesis: P = {} GX

A c= Q by A9;

then A12: union F c= Q by ZFMISC_1:76;

Q c= P \/ Q by XBOOLE_1:7;

then Q = P \/ Q by A5, A12;

hence P = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;now :: thesis: for B being Subset of GX st B in F & B <> A1 holds

B c= Q

then
for A being set st A in F holds B c= Q

let B be Subset of GX; :: thesis: ( B in F & B <> A1 implies B c= Q )

assume that

A10: B in F and

B <> A1 and

A11: not B c= Q ; :: thesis: contradiction

B is connected by A1, A10;

then ( B c= P or B c= Q ) by A5, A6, A10, Th16, ZFMISC_1:74;

hence contradiction by A4, A6, A9, A10, A11, Th7; :: thesis: verum

end;assume that

A10: B in F and

B <> A1 and

A11: not B c= Q ; :: thesis: contradiction

B is connected by A1, A10;

then ( B c= P or B c= Q ) by A5, A6, A10, Th16, ZFMISC_1:74;

hence contradiction by A4, A6, A9, A10, A11, Th7; :: thesis: verum

A c= Q by A9;

then A12: union F c= Q by ZFMISC_1:76;

Q c= P \/ Q by XBOOLE_1:7;

then Q = P \/ Q by A5, A12;

hence P = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

A13: now :: thesis: ( A1 c= P implies Q = {} GX )

A1 c= P \/ Q
by A3, A5, ZFMISC_1:74;assume A14:
A1 c= P
; :: thesis: Q = {} GX

A c= P by A14;

then A17: union F c= P by ZFMISC_1:76;

P c= P \/ Q by XBOOLE_1:7;

then P = P \/ Q by A5, A17;

hence Q = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

end;now :: thesis: for B being Subset of GX st B in F & B <> A1 holds

B c= P

then
for A being set st A in F holds B c= P

let B be Subset of GX; :: thesis: ( B in F & B <> A1 implies B c= P )

assume that

A15: B in F and

B <> A1 ; :: thesis: B c= P

B is connected by A1, A15;

then A16: ( B c= P or B c= Q ) by A5, A6, A15, Th16, ZFMISC_1:74;

assume not B c= P ; :: thesis: contradiction

hence contradiction by A4, A6, A14, A15, A16, Th7; :: thesis: verum

end;assume that

A15: B in F and

B <> A1 ; :: thesis: B c= P

B is connected by A1, A15;

then A16: ( B c= P or B c= Q ) by A5, A6, A15, Th16, ZFMISC_1:74;

assume not B c= P ; :: thesis: contradiction

hence contradiction by A4, A6, A14, A15, A16, Th7; :: thesis: verum

A c= P by A14;

then A17: union F c= P by ZFMISC_1:76;

P c= P \/ Q by XBOOLE_1:7;

then P = P \/ Q by A5, A17;

hence Q = {} GX by A7, XBOOLE_1:7, XBOOLE_1:28; :: thesis: verum

hence ( P = {} GX or Q = {} GX ) by A1, A3, A6, A13, A8, Th16; :: thesis: verum