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 )
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 ) )
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;
now :: thesis: ( ex A1 being Subset of GX st
( 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;
hence ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX ) by A1; :: thesis: verum