let GX be TopSpace; :: thesis: ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds

A = [#] GX )

A = [#] GX ) by A1; :: thesis: verum

A = [#] GX )

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

( P is open & P is closed & P <> {} GX & P <> [#] GX ) )

( P is open & P is closed & P <> {} GX & P <> [#] GX ) )

assume
not GX is connected
; :: thesis: ex P being Subset of GX st

( P is open & P is closed & P <> {} GX & P <> [#] GX )

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 ;

reconsider P = P, Q = Q as Subset of GX ;

Q = ([#] GX) \ P by A2, A3, Th1, PRE_TOPC:5;

then A6: P <> [#] GX by A5, PRE_TOPC:4;

( P is open & P is closed ) by A2, A3, Th4;

hence ex P being Subset of GX st

( P is open & P is closed & P <> {} GX & P <> [#] GX ) by A4, A6; :: thesis: verum

end;( P is open & P is closed & P <> {} GX & P <> [#] GX )

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 ;

reconsider P = P, Q = Q as Subset of GX ;

Q = ([#] GX) \ P by A2, A3, Th1, PRE_TOPC:5;

then A6: P <> [#] GX by A5, PRE_TOPC:4;

( P is open & P is closed ) by A2, A3, Th4;

hence ex P being Subset of GX st

( P is open & P is closed & P <> {} GX & P <> [#] GX ) by A4, A6; :: thesis: verum

now :: thesis: ( ex A1 being Subset of GX st

( A1 is open & A1 is closed & A1 <> {} GX & A1 <> [#] GX ) implies not GX is connected )

hence
( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds ( A1 is open & A1 is closed & A1 <> {} GX & A1 <> [#] GX ) implies not GX is connected )

given A1 being Subset of GX such that A7:
( A1 is open & A1 is closed )
and

A8: A1 <> {} GX and

A9: A1 <> [#] GX ; :: thesis: not GX is connected

A10: Cl (([#] GX) \ A1) = ([#] GX) \ A1 by A7, PRE_TOPC:23;

A11: A1 misses A1 ` by XBOOLE_1:79;

Cl A1 = A1 by A7, PRE_TOPC:22;

hence not GX is connected by A8, A9, A10, A11, Th12; :: thesis: verum

end;A8: A1 <> {} GX and

A9: A1 <> [#] GX ; :: thesis: not GX is connected

A10: Cl (([#] GX) \ A1) = ([#] GX) \ A1 by A7, PRE_TOPC:23;

A11: A1 misses A1 ` by XBOOLE_1:79;

Cl A1 = A1 by A7, PRE_TOPC:22;

hence not GX is connected by A8, A9, A10, A11, Th12; :: thesis: verum

A = [#] GX ) by A1; :: thesis: verum