let FT be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ([#] 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;

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ([#] 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 :: thesis: 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

hence
([#] FT) \ C is connected
by A1, Th6; :: thesis: verumQ = {} FT

A misses C1
by A9, SUBSET_1:23;

then A12: A /\ C1 = {} ;

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

A16: C is connected by A6, A11, Th37;

A23: Q c= ([#] FT) \ C by A13, XBOOLE_1:7;

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

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

A16: C is connected by A6, A11, Th37;

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

A22:
P misses P `
by XBOOLE_1:79;assume A18:
A c= Q
; :: thesis: 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; :: thesis: verum

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

A23: Q c= ([#] FT) \ C by A13, XBOOLE_1:7;

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

hence
( P = {} FT or Q = {} FT )
by A1, A4, A6, A10, A13, A15, A17, Th32; :: thesis: verumassume A24:
A c= P
; :: thesis: 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; :: thesis: verum

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