let GX be TopSpace; :: thesis: ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B )

A1: now

given A, B being Subset of GX such that A2: [#] GX = A \/ B and
A3: ( A <> {} GX & B <> {} GX ) and
A4: ( A is closed & B is closed & A misses B ) ; :: thesis: not GX is connected
A,B are_separated by A2, A4, Th3;
hence not GX is connected by A2, A3, Def2; :: thesis: verum

end;

now

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

end;

hence ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B ) by A1; :: thesis: verum