let GX be TopSpace; :: thesis: for A being Subset of GX holds
( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )
let A be Subset of GX; :: thesis: ( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )
A1: [#] (GX | A) = A by PRE_TOPC:def 5;

A2: now :: thesis: ( not A is connected implies ex P1, Q1 being Subset of GX st
( A = P1 \/ Q1 & P1,Q1 are_separated & P1 <> {} GX & Q1 <> {} GX ) )

assume not A is connected ; :: thesis: ex P1, Q1 being Subset of GX st
( A = P1 \/ Q1 & P1,Q1 are_separated & P1 <> {} GX & Q1 <> {} GX )
then not GX | A is connected ;
then consider P, Q being Subset of (GX | A) such that
A3: [#] (GX | A) = P \/ Q and
A4: P,Q are_separated and
A5: P <> {} (GX | A) and
A6: Q <> {} (GX | A) ;
reconsider Q1 = Q as Subset of GX by PRE_TOPC:11;
reconsider P1 = P as Subset of GX by PRE_TOPC:11;
P1,Q1 are_separated by A4, Th5;
hence ex P1, Q1 being Subset of GX st
( A = P1 \/ Q1 & P1,Q1 are_separated & P1 <> {} GX & Q1 <> {} GX ) by A1, A3, A5, A6; :: thesis: verum

end;

now :: thesis: ( ex P, Q being Subset of GX st
( A = P \/ Q & P,Q are_separated & P <> {} GX & Q <> {} GX ) implies not A is connected )

given P, Q being Subset of GX such that A7: A = P \/ Q and
A8: P,Q are_separated and
A9: P <> {} GX and
A10: Q <> {} GX ; :: thesis: not A is connected
reconsider Q1 = Q as Subset of (GX | A) by A1, A7, XBOOLE_1:7;
reconsider P1 = P as Subset of (GX | A) by A1, A7, XBOOLE_1:7;
P1,Q1 are_separated by A1, A7, A8, Th6;
then not GX | A is connected by A1, A7, A9, A10;
hence not A is connected ; :: thesis: verum

end;

hence ( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX ) by A2; :: thesis: verum