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 ;
now :: thesis: for P, Q being Subset of GX st union F = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} 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 = {} ;
A8: now :: thesis: ( A1 c= Q implies P = {} GX )
assume A9: A1 c= Q ; :: thesis: P = {} GX
now :: thesis: for B being Subset of GX st B in F & B <> A1 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;
then for A being set st A in F holds
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;
A13: now :: thesis: ( A1 c= P implies Q = {} GX )
assume A14: A1 c= P ; :: thesis: Q = {} GX
now :: thesis: for B being Subset of GX st B in F & B <> A1 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;
then for A being set st A in F holds
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;
A1 c= P \/ Q by A3, A5, ZFMISC_1:74;
hence ( P = {} GX or Q = {} GX ) by A1, A3, A6, A13, A8, Th16; :: thesis: verum
end;
hence union F is connected by Th15; :: thesis: verum