let GX be TopSpace; :: thesis: ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX )

A1: now

given A1 being Subset of GX such that A2: ( A1 is open & A1 is closed & A1 <> {} GX & A1 <> [#] GX ) ; :: thesis: not GX is connected
A3: ( Cl A1 = A1 & Cl (([#] GX) \ A1) = ([#] GX) \ A1 ) by A2, PRE_TOPC:52, PRE_TOPC:53;
A1 misses A1 ` by XBOOLE_1:79;
hence not GX is connected by A2, A3, Th13; :: thesis: verum

end;

now

assume not GX is connected ; :: thesis: ex P being Subset of GX st
( P is open & P is closed & P <> {} GX & P <> [#] GX )
then consider P, Q being Subset of GX such that
A4: [#] GX = P \/ Q and
A5: P,Q are_separated and
A6: ( P <> {} GX & Q <> {} GX ) by Def2;
reconsider P = P, Q = Q as Subset of GX ;
A7: ( P is open & P is closed & Q is open & Q is closed ) by A4, A5, Th5;
Q = ([#] GX) \ P by A4, A5, Th2, PRE_TOPC:25;
then P <> [#] GX by A6, PRE_TOPC:23;
hence ex P being Subset of GX st
( P is open & P is closed & P <> {} GX & P <> [#] GX ) by A6, A7; :: thesis: verum

end;

hence ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX ) by A1; :: thesis: verum