let FT be non empty RelStr ; for A, C being Subset of FT
for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected
let A, C be Subset of FT; for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected
let D be non empty Subset of FT; ( FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D implies ([#] FT) \ C is connected )
assume that
A1:
( FT is filled & FT is symmetric )
and
A2:
D = ([#] FT) \ A
and
A3:
FT is connected
and
A4:
A is connected
and
A5:
C is_a_component_of D
; ([#] FT) \ C is connected
consider C1 being Subset of (FT | D) such that
A6:
C1 = C
and
A7:
C1 is_a_component_of FT | D
by A5;
reconsider C2 = C1 as Subset of FT by A6;
C1 c= [#] (FT | D)
;
then
C1 c= ([#] FT) \ A
by A2, Def3;
then A8:
(([#] FT) \ A) ` c= C2 `
by SUBSET_1:12;
then A9:
A c= C2 `
by PRE_TOPC:3;
A10:
A c= ([#] FT) \ C2
by A8, PRE_TOPC:3;
A11:
C1 is connected
by A7;
now for P, Q being Subset of FT st ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT
A misses C1
by A9, SUBSET_1:23;
then A12:
A /\ C1 = {}
;
let P,
Q be
Subset of
FT;
( ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT )assume that A13:
([#] FT) \ C = P \/ Q
and A14:
P misses Q
and A15:
P,
Q are_separated
;
( P = {} FT or Q = {} FT )A16:
C is
connected
by A6, A11, Th37;
A17:
now ( A c= Q implies P = {} FT )assume A18:
A c= Q
;
P = {} FT
P c= Q `
by A14, SUBSET_1:23;
then
(
Q misses Q ` &
A /\ P c= Q /\ (Q `) )
by A18, XBOOLE_1:27, XBOOLE_1:79;
then A19:
A /\ P c= {}
;
(C \/ P) /\ A =
(A /\ C) \/ (A /\ P)
by XBOOLE_1:23
.=
{}
by A6, A12, A19, XBOOLE_1:3
;
then
C \/ P misses A
;
then
C \/ P c= A `
by SUBSET_1:23;
then
C \/ P c= [#] (FT | D)
by A2, Def3;
then reconsider C1P1 =
C \/ P as
Subset of
(FT | D) ;
C \/ P is
connected
by A1, A3, A13, A15, A16, Th36;
then A20:
C1P1 is
connected
by Th37;
C c= C1 \/ P
by A6, XBOOLE_1:7;
then
C1P1 = C1
by A6, A7, A20;
then A21:
P c= C
by A6, XBOOLE_1:7;
P c= ([#] FT) \ C
by A13, XBOOLE_1:7;
then
(
C misses C ` &
P c= C /\ (([#] FT) \ C) )
by A21, XBOOLE_1:19, XBOOLE_1:79;
then
P c= {}
;
hence
P = {} FT
by XBOOLE_1:3;
verum end; A22:
P misses P `
by XBOOLE_1:79;
A23:
Q c= ([#] FT) \ C
by A13, XBOOLE_1:7;
now ( A c= P implies Q = {} FT )assume A24:
A c= P
;
Q = {} FT
Q c= P `
by A14, SUBSET_1:23;
then
A /\ Q c= P /\ (P `)
by A24, XBOOLE_1:27;
then A25:
A /\ Q c= {}
by A22;
(C \/ Q) /\ A =
(A /\ C) \/ (A /\ Q)
by XBOOLE_1:23
.=
{}
by A6, A12, A25, XBOOLE_1:3
;
then
C \/ Q misses A
;
then
C \/ Q c= A `
by SUBSET_1:23;
then
C \/ Q c= [#] (FT | D)
by A2, Def3;
then reconsider C1Q1 =
C \/ Q as
Subset of
(FT | D) ;
C \/ Q is
connected
by A1, A3, A13, A15, A16, Th36;
then A26:
C1Q1 is
connected
by Th37;
C1 c= C1 \/ Q
by XBOOLE_1:7;
then
C1Q1 = C1
by A6, A7, A26;
then
Q c= C
by A6, XBOOLE_1:7;
then
(
C misses C ` &
Q c= C /\ (([#] FT) \ C) )
by A23, XBOOLE_1:19, XBOOLE_1:79;
then
Q c= {}
;
hence
Q = {} FT
by XBOOLE_1:3;
verum end; hence
(
P = {} FT or
Q = {} FT )
by A1, A4, A6, A10, A13, A15, A17, Th32;
verum end;
hence
([#] FT) \ C is connected
by A1, Th6; verum