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) )

Cl A meets Cl (([#] GX) \ A) ) by A1; :: thesis: verum

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 )

( 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;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

now :: thesis: ( not GX is connected implies ex A being Subset of GX st

( A <> {} GX & A <> [#] GX & Cl A misses Cl (([#] GX) \ A) ) )

hence
( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds ( 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;( 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

Cl A meets Cl (([#] GX) \ A) ) by A1; :: thesis: verum