let G be non empty symmetric RelStr ; :: thesis:
let x be Element of G; :: thesis:
let R1, R2 be non empty RelStr ; :: thesis:
assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr (([#] G) \ {x}) = union_of (R1,R2) and
A3: G is path-connected ; :: thesis:
set R = subrelstr (([#] G) \ {x});
set A = the carrier of (subrelstr (([#] G) \ {x}));
the carrier of R1 c= the carrier of R1 \/ the carrier of R2 by XBOOLE_1:7;
then A4: the carrier of R1 c= the carrier of (subrelstr (([#] G) \ {x})) by A2, NECKLA_2:def 2;
set a = the Element of R1;
A5: the carrier of (subrelstr (([#] G) \ {x})) = ([#] G) \ {x} by YELLOW_0:def 15;
A6: x <> the Element of R1

proof

assume not x <> the Element of R1 ; :: thesis:
then x in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then x in the carrier of G \ {x} by A2, A5, NECKLA_2:def 2;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

reconsider A = the carrier of (subrelstr (([#] G) \ {x})) as Subset of G by YELLOW_0:def 15;
A7: the carrier of (subrelstr (([#] G) \ {x})) = A ;
then the carrier of R1 c= the carrier of G by A4, XBOOLE_1:1;
then the Element of R1 in the carrier of G ;
then the InternalRel of G reduces x, the Element of R1 by A3, A6;
then consider p being FinSequence such that
A8: len p > 0 and
A9: p . 1 = x and
A10: p . (len p) = the Element of R1 and
A11: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of G by REWRITE1:11;
defpred S₁[ Nat] means ( p . $1 in the carrier of R1 & $1 in dom p & ( for k being Nat st k > $1 & k in dom p holds
p . k in the carrier of R1 ) );
S₁[ len p] by A8, A10, CARD_1:27, FINSEQ_3:25, FINSEQ_5:6;
then A12: ex k being Nat st S₁[k] ;
ex n0 being Nat st
( S₁[n0] & ( for n being Nat st S₁[n] holds
n >= n0 ) ) from NAT_1:sch 5(A12);
then consider n0 being Element of NAT such that
A13: S₁[n0] and
A14: for n being Nat st S₁[n] holds
n >= n0 ;
n0 <> 0

proof

assume not n0 <> 0 ; :: thesis:
then 0 in Seg (len p) by A13, FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1; :: thesis:

end;

then consider k0 being Nat such that
A15: n0 = k0 + 1 by NAT_1:6;
A16: n0 <> 1

proof

assume not n0 <> 1 ; :: thesis:
then not x in {x} by A5, A4, A9, A13, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

A17: k0 >= 1

proof

assume not k0 >= 1 ; :: thesis:
then k0 = 0 by NAT_1:25;
hence contradiction by A15, A16; :: thesis:

end;

n0 in Seg (len p) by A13, FINSEQ_1:def 3;
then A18: n0 <= len p by FINSEQ_1:1;
A19: k0 < n0 by A15, NAT_1:13;
A20: for k being Nat st k > k0 & k in dom p holds
p . k in the carrier of R1

proof

assume ex k being Nat st
( k > k0 & k in dom p & not p . k in the carrier of R1 ) ; :: thesis:
then consider k being Nat such that
A21: k > k0 and
A22: k in dom p and
A23: not p . k in the carrier of R1 ;
k > n0

proof

per cases by XXREAL_0:1;

suppose k < n0 ; :: thesis:

hence k > n0 by A15, A21, NAT_1:13; :: thesis:

end;

suppose n0 < k ; :: thesis:

hence k > n0 ; :: thesis:

end;

suppose n0 = k ; :: thesis:

hence k > n0 by A13, A23; :: thesis:

end;

hence contradiction by A13, A22, A23; :: thesis:

end;

A24: the carrier of G = the carrier of (subrelstr (([#] G) \ {x})) \/ {x}

proof

thus the carrier of G c= the carrier of (subrelstr (([#] G) \ {x})) \/ {x} :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: a in the carrier of G ; :: thesis:

per cases ;

suppose a = x ; :: thesis:

then a in {x} by TARSKI:def 1;
hence a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} by XBOOLE_0:def 3; :: thesis:

end;

suppose a <> x ; :: thesis:

then not a in {x} by TARSKI:def 1;
then a in A by A5, A25, XBOOLE_0:def 5;
hence a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} by XBOOLE_0:def 3; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} ; :: thesis:

per cases by A26, XBOOLE_0:def 3;

suppose a in the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis:

hence a in the carrier of G by A5; :: thesis:

end;

suppose a in {x} ; :: thesis:

hence a in the carrier of G ; :: thesis:

end;

k0 <= n0 by A15, XREAL_1:29;
then k0 <= len p by A18, XXREAL_0:2;
then A27: k0 in dom p by A17, FINSEQ_3:25;
then A28: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A11, A13, A15;
then A29: p . k0 in the carrier of G by ZFMISC_1:87;
thus ex b being Element of R1 st [b,x] in the InternalRel of G :: thesis:

proof

per cases by A29, A24, XBOOLE_0:def 3;

suppose A30: p . k0 in the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis:

set u = p . k0;
set v = p . n0;
[(p . k0),(p . n0)] in [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] by A4, A13, A30, ZFMISC_1:87;
then A31: [(p . k0),(p . n0)] in the InternalRel of G |_2 the carrier of (subrelstr (([#] G) \ {x})) by A15, A28, XBOOLE_0:def 4;
p . k0 in the carrier of R1 \/ the carrier of R2 by A2, A30, NECKLA_2:def 2;
then ( p . k0 in the carrier of R1 or p . k0 in the carrier of R2 ) by XBOOLE_0:def 3;
then reconsider u = p . k0 as Element of R2 by A14, A27, A19, A20;
reconsider v = p . n0 as Element of R1 by A13;
not [u,v] in the InternalRel of (subrelstr (([#] G) \ {x}))

proof

u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A32: u in the carrier of (subrelstr (([#] G) \ {x})) by A2, NECKLA_2:def 2;
A33: ( v in the carrier of R1 & the InternalRel of (subrelstr (([#] G) \ {x})) is_symmetric_in the carrier of (subrelstr (([#] G) \ {x})) ) by NECKLACE:def 3;
assume [u,v] in the InternalRel of (subrelstr (([#] G) \ {x})) ; :: thesis:
then [v,u] in the InternalRel of (subrelstr (([#] G) \ {x})) by A4, A32, A33;
hence contradiction by A1, A2, Th35; :: thesis:

end;

hence ex b being Element of R1 st [b,x] in the InternalRel of G by A31, YELLOW_0:def 14; :: thesis:

end;

suppose A34: p . k0 in {x} ; :: thesis:

set b = p . n0;
reconsider b = p . n0 as Element of R1 by A13;
A35: ( b in the carrier of (subrelstr (([#] G) \ {x})) & the InternalRel of G is_symmetric_in the carrier of G ) by A4, NECKLACE:def 3;
p . k0 = x by A34, TARSKI:def 1;
then [b,x] in the InternalRel of G by A7, A15, A28, A35;
hence ex b being Element of R1 st [b,x] in the InternalRel of G ; :: thesis:

end;