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

([#] 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 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 :: thesis: for P, Q being Subset of GX st ([#] GX) \ C = P \/ Q & P,Q are_separated & not P = {} GX holds

Q = {} GX

hence
([#] GX) \ C is connected
by Th15; :: thesis: verumQ = {} 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; :: thesis: ( ([#] 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 ; :: thesis: ( P = {} GX or Q = {} GX )

A11: P misses P ` by XBOOLE_1:79;

A12: P misses Q by A10, Th1;

end;then A7: A /\ C1 = {} ;

A8: C is connected by A4, A5, Th23;

let P, Q be Subset of GX; :: thesis: ( ([#] 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 ; :: thesis: ( P = {} GX or Q = {} GX )

A11: P misses P ` by XBOOLE_1:79;

A12: P misses Q by A10, Th1;

A13: now :: thesis: ( A c= Q implies P = {} GX )

A20:
Q c= ([#] GX) \ C
by A9, XBOOLE_1:7;A14:
Q misses Q `
by XBOOLE_1:79;

assume A15: A c= Q ; :: thesis: 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 ; :: thesis: verum

end;assume A15: A c= Q ; :: thesis: 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 ; :: thesis: verum

now :: thesis: ( A c= P implies Q = {} GX )

hence
( P = {} GX or Q = {} GX )
by A2, A4, A6, A9, A10, A13, Th16; :: thesis: verumassume A21:
A c= P
; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum