let GX be TopSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ([#] GX) \ C is connected
consider C1 being Subset of (GX | (([#] GX) \ A)) such that
A4: C1 = C and
A5: C1 is_a_component_of GX | (([#] GX) \ A) by A3, Def6;
reconsider C2 = C1 as Subset of GX by A4;
C1 c= [#] (GX | (([#] GX) \ A)) ;
then C1 c= ([#] GX) \ A by PRE_TOPC:def 10;
then (([#] GX) \ A) ` c= C2 ` by SUBSET_1:31;
then A6: A c= C2 ` by PRE_TOPC:22;
A7: C1 is connected by A5, Def5;

now

A misses C1 by A6, SUBSET_1:43;
then A8: A /\ C1 = {} by XBOOLE_0:def 7;
A9: C is connected by A4, A7, Th24;
let P, Q be Subset of GX; :: thesis: ( ([#] GX) \ C = P \/ Q & P,Q are_separated & not P = {} GX implies Q = {} GX )
assume that
A10: ([#] GX) \ C = P \/ Q and
A11: P,Q are_separated ; :: thesis: ( P = {} GX or Q = {} GX )
A12: P misses P ` by XBOOLE_1:79;
A13: P misses Q by A11, Th2;

A14: now

A15: Q misses Q ` by XBOOLE_1:79;
assume A16: A c= Q ; :: thesis: P = {} GX
P c= Q ` by A13, SUBSET_1:43;
then A /\ P c= Q /\ (Q ` ) by A16, XBOOLE_1:27;
then A17: A /\ P c= {} by A15, XBOOLE_0:def 7;
(C \/ P) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by A4, A8, A17 ;
then C \/ P misses A by XBOOLE_0:def 7;
then C \/ P c= A ` by SUBSET_1:43;
then C \/ P c= [#] (GX | (([#] GX) \ A)) by PRE_TOPC:def 10;
then reconsider C1P1 = C \/ P as Subset of (GX | (([#] GX) \ A)) ;
A18: C misses C ` by XBOOLE_1:79;
C \/ P is connected by A1, A10, A11, A9, Th21;
then A19: C1P1 is connected by Th24;
C c= C1 \/ P by A4, XBOOLE_1:7;
then C1P1 = C1 by A4, A5, A19, Def5;
then A20: P c= C by A4, XBOOLE_1:7;
P c= ([#] GX) \ C by A10, XBOOLE_1:7;
then P c= C /\ (([#] GX) \ C) by A20, XBOOLE_1:19;
then P c= {} by A18, XBOOLE_0:def 7;
hence P = {} GX ; :: thesis: verum

end;

A21: Q c= ([#] GX) \ C by A10, XBOOLE_1:7;

now

assume A22: A c= P ; :: thesis: Q = {} GX
Q c= P ` by A13, SUBSET_1:43;
then A /\ Q c= P /\ (P ` ) by A22, XBOOLE_1:27;
then A23: A /\ Q c= {} by A12, XBOOLE_0:def 7;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by A4, A8, A23 ;
then C \/ Q misses A by XBOOLE_0:def 7;
then C \/ Q c= A ` by SUBSET_1:43;
then C \/ Q c= [#] (GX | (([#] GX) \ A)) by PRE_TOPC:def 10;
then reconsider C1Q1 = C \/ Q as Subset of (GX | (([#] GX) \ A)) ;
C \/ Q is connected by A1, A10, A11, A9, Th21;
then A24: C1Q1 is connected by Th24;
C1 c= C1 \/ Q by XBOOLE_1:7;
then C1Q1 = C1 by A4, A5, A24, Def5;
then Q c= C by A4, XBOOLE_1:7;
then A25: Q c= C /\ (([#] GX) \ C) by A21, XBOOLE_1:19;
C misses C ` by XBOOLE_1:79;
then Q c= {} by A25, XBOOLE_0:def 7;
hence Q = {} GX ; :: thesis: verum

end;

hence ( P = {} GX or Q = {} GX ) by A2, A4, A6, A10, A11, A14, Th17; :: thesis: verum

end;

hence ([#] GX) \ C is connected by Th16; :: thesis: verum