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 & {} (GX | A) = {} )
by PRE_TOPC:def 10;
A2:
now given P,
Q being
Subset of
GX such that A3:
A = P \/ Q
and A4:
P,
Q are_separated
and A5:
(
P <> {} GX &
Q <> {} GX )
;
:: thesis: not A is connected reconsider P1 =
P as
Subset of
(GX | A) by A1, A3, XBOOLE_1:7;
reconsider Q1 =
Q as
Subset of
(GX | A) by A1, A3, XBOOLE_1:7;
P1,
Q1 are_separated
by A1, A3, A4, Th7;
then
not
GX | A is
connected
by A1, A3, A5, Def2;
hence
not
A is
connected
by Def3;
:: thesis: verum end;
now 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
by Def3;
then consider P,
Q being
Subset of
(GX | A) such that A6:
[#] (GX | A) = P \/ Q
and A7:
P,
Q are_separated
and A8:
(
P <> {} (GX | A) &
Q <> {} (GX | A) )
by Def2;
reconsider P1 =
P as
Subset of
GX by PRE_TOPC:39;
reconsider Q1 =
Q as
Subset of
GX by PRE_TOPC:39;
P1,
Q1 are_separated
by A7, Th6;
hence
ex
P1,
Q1 being
Subset of
GX st
(
A = P1 \/ Q1 &
P1,
Q1 are_separated &
P1 <> {} GX &
Q1 <> {} GX )
by A1, A6, A8;
:: 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