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;
A6: now :: thesis: for B being Subset of GX st B in F & B <> A2 holds
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;
A2 <> {} GX by A4;
hence union F is connected by A1, A5, A6, Th25; :: thesis: verum