let GX be TopSpace; for A, C being Subset of GX st GX is connected & A is connected & C is_a_component_of ([#] GX) \ A holds
([#] GX) \ C is connected
let A, C be Subset of GX; ( GX is connected & A is connected & C is_a_component_of ([#] GX) \ A implies ([#] GX) \ C is connected )
assume that
A1:
GX is connected
and
A2:
A is connected
and
A3:
C is_a_component_of ([#] GX) \ A
; ([#] GX) \ C is connected
consider C1 being Subset of (GX | (([#] GX) \ A)) such that
A4:
C1 = C
and
A5:
C1 is a_component
by A3;
reconsider C2 = C1 as Subset of GX by A4;
C1 c= [#] (GX | (([#] GX) \ A))
;
then
C1 c= ([#] GX) \ A
by PRE_TOPC:def 5;
then
(([#] GX) \ A) ` c= C2 `
by SUBSET_1:12;
then A6:
A c= C2 `
by PRE_TOPC:3;
now for P, Q being Subset of GX st ([#] GX) \ C = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX
A misses C1
by A6, SUBSET_1:23;
then A7:
A /\ C1 = {}
;
A8:
C is
connected
by A4, A5, Th23;
let P,
Q be
Subset of
GX;
( ([#] GX) \ C = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )assume that A9:
([#] GX) \ C = P \/ Q
and A10:
P,
Q are_separated
;
( P = {} GX or Q = {} GX )A11:
P misses P `
by XBOOLE_1:79;
A12:
P misses Q
by A10, Th1;
A13:
now ( A c= Q implies P = {} GX )A14:
Q misses Q `
by XBOOLE_1:79;
assume A15:
A c= Q
;
P = {} GX
P c= Q `
by A12, SUBSET_1:23;
then
A /\ P c= Q /\ (Q `)
by A15, XBOOLE_1:27;
then A16:
A /\ P c= {}
by A14;
(C \/ P) /\ A =
(A /\ C) \/ (A /\ P)
by XBOOLE_1:23
.=
{}
by A4, A7, A16
;
then
C \/ P misses A
;
then
C \/ P c= A `
by SUBSET_1:23;
then
C \/ P c= [#] (GX | (([#] GX) \ A))
by PRE_TOPC:def 5;
then reconsider C1P1 =
C \/ P as
Subset of
(GX | (([#] GX) \ A)) ;
A17:
C misses C `
by XBOOLE_1:79;
C \/ P is
connected
by A1, A9, A10, A8, Th20;
then A18:
C1P1 is
connected
by Th23;
C c= C1 \/ P
by A4, XBOOLE_1:7;
then
C1P1 = C1
by A4, A5, A18;
then A19:
P c= C
by A4, XBOOLE_1:7;
P c= ([#] GX) \ C
by A9, XBOOLE_1:7;
then
P c= C /\ (([#] GX) \ C)
by A19, XBOOLE_1:19;
then
P c= {}
by A17;
hence
P = {} GX
;
verum end; A20:
Q c= ([#] GX) \ C
by A9, XBOOLE_1:7;
now ( A c= P implies Q = {} GX )assume A21:
A c= P
;
Q = {} GX
Q c= P `
by A12, SUBSET_1:23;
then
A /\ Q c= P /\ (P `)
by A21, XBOOLE_1:27;
then A22:
A /\ Q c= {}
by A11;
(C \/ Q) /\ A =
(A /\ C) \/ (A /\ Q)
by XBOOLE_1:23
.=
{}
by A4, A7, A22
;
then
C \/ Q misses A
;
then
C \/ Q c= A `
by SUBSET_1:23;
then
C \/ Q c= [#] (GX | (([#] GX) \ A))
by PRE_TOPC:def 5;
then reconsider C1Q1 =
C \/ Q as
Subset of
(GX | (([#] GX) \ A)) ;
C \/ Q is
connected
by A1, A9, A10, A8, Th20;
then A23:
C1Q1 is
connected
by Th23;
C1 c= C1 \/ Q
by XBOOLE_1:7;
then
C1Q1 = C1
by A4, A5, A23;
then
Q c= C
by A4, XBOOLE_1:7;
then A24:
Q c= C /\ (([#] GX) \ C)
by A20, XBOOLE_1:19;
C misses C `
by XBOOLE_1:79;
then
Q c= {}
by A24;
hence
Q = {} GX
;
verum end; hence
(
P = {} GX or
Q = {} GX )
by A2, A4, A6, A9, A10, A13, Th16;
verum end;
hence
([#] GX) \ C is connected
by Th15; verum