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

given A, B being Subset of GX such that A2: [#] GX = A \/ B and
A3: ( A <> {} GX & B <> {} GX ) and
A4: ( A is open & B is open ) and
A5: A misses B ; :: thesis: not GX is connected
A,B are_separated by A2, A4, A5, Th4;
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 open & B is open & A misses B )
then consider P, Q being Subset of GX such that
A6: [#] GX = P \/ Q and
A7: P,Q are_separated and
A8: ( P <> {} GX & Q <> {} GX ) by Def2;
reconsider P = P, Q = Q as Subset of GX ;
( P is open & Q is open ) by A6, A7, 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 A6, A7, A8, 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 open & B is open holds
A meets B ) by A1; :: thesis: verum