let G be non empty symmetric RelStr ; :: thesis: for x being Element of G
for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected holds
ex b being Element of R1 st [b,x] in the InternalRel of G
let x be Element of G; :: thesis: for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected holds
ex b being Element of R1 st [b,x] in the InternalRel of G
let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected implies ex b being Element of R1 st [b,x] in the InternalRel of G )
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: ex b being Element of R1 st [b,x] in the InternalRel of G
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: contradiction
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: verum
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 S1[ 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 ) );
S1[ len p] by A8, A10, CARD_1:27, FINSEQ_3:25, FINSEQ_5:6;
then A12: ex k being Nat st S1[k] ;
ex n0 being Nat st
( S1[n0] & ( for n being Nat st S1[n] holds
n >= n0 ) ) from NAT_1:sch 5(A12);
 then consider n0 being Element of NAT such that
A13: S1[n0] and
A14: for n being Nat st S1[n] holds
n >= n0 ;
n0 <> 0
proof
assume not n0 <> 0 ; :: thesis: contradiction
then 0 in Seg (len p) by A13, FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1; :: thesis: verum
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: contradiction
then not x in {x} by A5, A4, A9, A13, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A17: k0 >= 1
proof
assume not k0 >= 1 ; :: thesis: contradiction
then k0 = 0 by NAT_1:25;
hence contradiction by A15, A16; :: thesis: verum
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: contradiction
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 ( k < n0 or n0 < k or n0 = k ) by XXREAL_0:1;
suppose k < n0 ; :: thesis: k > n0
hence k > n0 by A15, A21, NAT_1:13; :: thesis: verum
end;
suppose n0 < k ; :: thesis: k > n0
hence k > n0 ; :: thesis: verum
end;
suppose n0 = k ; :: thesis: k > n0
hence k > n0 by A13, A23; :: thesis: verum
end;
end;
end;
hence contradiction by A13, A22, A23; :: thesis: verum
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: the carrier of (subrelstr (([#] G) \ {x})) \/ {x} c= the carrier of G
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of G or a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} )
assume A25: a in the carrier of G ; :: thesis: a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x}
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} or a in the carrier of G )
assume A26: a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} ; :: thesis: a in the carrier of G
per cases ( a in the carrier of (subrelstr (([#] G) \ {x})) or a in {x} ) by A26, XBOOLE_0:def 3;
suppose a in the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis: a in the carrier of G
hence a in the carrier of G by A5; :: thesis: verum
end;
suppose a in {x} ; :: thesis: a in the carrier of G
hence a in the carrier of G ; :: thesis: verum
end;
end;
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: verum
proof
per cases ( p . k0 in the carrier of (subrelstr (([#] G) \ {x})) or p . k0 in {x} ) by A29, A24, XBOOLE_0:def 3;
suppose A30: p . k0 in the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis: ex b being Element of R1 st [b,x] in the InternalRel of G
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: contradiction
then [v,u] in the InternalRel of (subrelstr (([#] G) \ {x})) by A4, A32, A33;
hence contradiction by A1, A2, Th35; :: thesis: verum
end;
hence ex b being Element of R1 st [b,x] in the InternalRel of G by A31, YELLOW_0:def 14; :: thesis: verum
end;
suppose A34: p . k0 in {x} ; :: thesis: ex b being Element of R1 st [b,x] in the InternalRel of G
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: verum
end;
end;
end;