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 A5, XBOOLE_1:3, XBOOLE_1:27;
then A6: A misses Cl (([#] GX) \ A) ;
A7: [#] GX = A \/ (A `) by PRE_TOPC:2;
A8: ([#] GX) \ A <> {} GX by A3, PRE_TOPC:4;
([#] GX) \ A c= Cl (([#] GX) \ A) by PRE_TOPC:18;
then (Cl A) /\ (([#] GX) \ A) = {} by A5, XBOOLE_1:3, XBOOLE_1:27;
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 A12, PRE_TOPC:22;
A16: Cl B = B by A13, PRE_TOPC:22;
A17: B = ([#] GX) \ A by A9, A14, PRE_TOPC:5;
then A <> [#] GX by A11, PRE_TOPC:4;
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