for GX being TopSpace
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