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

A1: now :: thesis: ( ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) ) implies not GX is connected )
given A being Subset of GX such that A2: A <> {} GX and
A3: A <> [#] GX and
A4: Cl A misses Cl (([#] GX) \ A) ; :: thesis: not GX is connected
A5: (Cl A) /\ (Cl (([#] GX) \ A)) = {} by A4;
A c= Cl A by PRE_TOPC:18;
then A /\ (Cl (([#] GX) \ A)) = {} GX by ;
then A6: A misses Cl (([#] GX) \ A) ;
A7: [#] GX = A \/ (A `) by PRE_TOPC:2;
A8: ([#] GX) \ A <> {} GX by ;
([#] GX) \ A c= Cl (([#] GX) \ A) by PRE_TOPC:18;
then (Cl A) /\ (([#] GX) \ A) = {} by ;
then Cl A misses ([#] GX) \ A ;
then A,([#] GX) \ A are_separated by A6;
hence not GX is connected by A2, A8, A7; :: thesis: verum
end;
now :: thesis: ( not GX is connected implies ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) ) )
assume not GX is connected ; :: thesis: ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) )

then consider A, B being Subset of GX such that
A9: [#] GX = A \/ B and
A10: A <> {} GX and
A11: B <> {} GX and
A12: A is closed and
A13: B is closed and
A14: A misses B by Th10;
A15: Cl A = A by ;
A16: Cl B = B by ;
A17: B = ([#] GX) \ A by ;
then A <> [#] GX by ;
hence ex A being Subset of GX st
( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) ) by A10, A14, A17, A15, A16; :: thesis: verum
end;
hence ( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds
Cl A meets Cl (([#] GX) \ A) ) by A1; :: thesis: verum