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;

Q = {} GX ) by A2; :: thesis: verum

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

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

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 )

hence
( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds ( 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;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

Q = {} GX ) by A2; :: thesis: verum