let GX be TopSpace; 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; ( 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 ( 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
;
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;
verum end;
now ( 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
;
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
;
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; verum