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 open & B is open holds
A meets B )

A1: now

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

end;

now

given A, B being Subset of GX such that A7: [#] GX = A \/ B and
A8: A <> {} GX and
A9: B <> {} GX and
A10: A is open and
A11: B is open and
A12: A misses B ; :: thesis: not GX is connected
A,B are_separated by A7, A10, A11, A12, Th4;
hence not GX is connected by A7, A8, A9, Def2; :: 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 open & B is open holds
A meets B ) by A1; :: thesis: verum