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}));
A4: the carrier of (subrelstr (([#] G) \ {x})) = ([#] G) \ {x} by YELLOW_0:def 15;
reconsider A = the carrier of (subrelstr (([#] G) \ {x})) as Subset of G by YELLOW_0:def 15;
consider a being Element of R1;
the carrier of R1 c= the carrier of R1 \/ the carrier of R2 by XBOOLE_1:7;
then A5: the carrier of R1 c= the carrier of (subrelstr (([#] G) \ {x})) by A2, NECKLA_2:def 2;
A6: the carrier of (subrelstr (([#] G) \ {x})) = A ;
then the carrier of R1 c= the carrier of G by A5, XBOOLE_1:1;
then A7: a in the carrier of G by TARSKI:def 3;
x <> a
proof
assume not x <> a ; :: 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, A4, NECKLA_2:def 2;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
then the InternalRel of G reduces x,a by A3, A7, Def2;
then consider p being FinSequence such that
A8: ( len p > 0 & p . 1 = x & p . (len p) = a ) and
A9: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of G by REWRITE1:12;
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 ) );
A10: ex k being Nat st S1[k]
proof
S1[ len p] by A8, CARD_1:47, FINSEQ_3:27, FINSEQ_5:6;
hence ex k being Nat st S1[k] ; :: thesis: verum
end;
ex n0 being Nat st
( S1[n0] & ( for n being Nat st S1[n] holds
n >= n0 ) ) from NAT_1:sch 5(A10);
 then consider n0 being Element of NAT such that
A11: S1[n0] and
A12: 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 A11, FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:3; :: thesis: verum
end;
then consider k0 being Nat such that
A13: n0 = k0 + 1 by NAT_1:6;
A14: n0 <> 1
proof
assume not n0 <> 1 ; :: thesis: contradiction
then ( x in the carrier of G & not x in {x} ) by A4, A5, A8, A11, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A15: k0 >= 1
proof
assume not k0 >= 1 ; :: thesis: contradiction
then k0 = 0 by NAT_1:26;
hence contradiction by A13, A14; :: thesis: verum
end;
k0 <= len p
proof
A16: k0 <= n0 by A13, XREAL_1:31;
n0 in Seg (len p) by A11, FINSEQ_1:def 3;
then n0 <= len p by FINSEQ_1:3;
hence k0 <= len p by A16, XXREAL_0:2; :: thesis: verum
end;
then A17: k0 in dom p by A15, FINSEQ_3:27;
A18: k0 < n0 by A13, NAT_1:13;
A19: 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
A20: ( k > k0 & k in dom p & 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 A13, A20, 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 A11, A20; :: thesis: verum
end;
end;
end;
hence contradiction by A11, A20; :: thesis: verum
end;
A21: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A9, A11, A13, A17;
then A22: ( p . k0 in the carrier of G & p . n0 in the carrier of G ) by A13, ZFMISC_1:106;
A23: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of G or a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} )
assume A24: a in the carrier of G ; :: thesis: a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x}
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x} or a in the carrier of G )
assume A25: 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 A25, 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 A4; :: 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;
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 A22, A23, XBOOLE_0:def 3;
suppose A26: p . k0 in the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis: ex b being Element of R1 st [b,x] in the InternalRel of G
then p . k0 in the carrier of R1 \/ the carrier of R2 by A2, NECKLA_2:def 2;
then A27: ( p . k0 in the carrier of R1 or p . k0 in the carrier of R2 ) by XBOOLE_0:def 3;
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 A5, A11, A26, ZFMISC_1:106;
then A28: [(p . k0),(p . n0)] in the InternalRel of G |_2 the carrier of (subrelstr (([#] G) \ {x})) by A13, A21, XBOOLE_0:def 4;
reconsider u = p . k0 as Element of R2 by A12, A17, A18, A19, A27;
reconsider v = p . n0 as Element of R1 by A11;
not [u,v] in the InternalRel of (subrelstr (([#] G) \ {x}))
proof
assume A29: [u,v] in the InternalRel of (subrelstr (([#] G) \ {x})) ; :: thesis: contradiction
A30: v in the carrier of R1 ;
u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A31: u in the carrier of (subrelstr (([#] G) \ {x})) by A2, NECKLA_2:def 2;
the InternalRel of (subrelstr (([#] G) \ {x})) is_symmetric_in the carrier of (subrelstr (([#] G) \ {x})) by NECKLACE:def 4;
then [v,u] in the InternalRel of (subrelstr (([#] G) \ {x})) by A5, A29, A30, A31, RELAT_2:def 3;
hence contradiction by A1, A2, Th36; :: thesis: verum
end;
hence ex b being Element of R1 st [b,x] in the InternalRel of G by A28, YELLOW_0:def 14; :: thesis: verum
end;
suppose p . k0 in {x} ; :: thesis: ex b being Element of R1 st [b,x] in the InternalRel of G
then A32: p . k0 = x by TARSKI:def 1;
set b = p . n0;
reconsider b = p . n0 as Element of R1 by A11;
A33: b in the carrier of (subrelstr (([#] G) \ {x})) by A5, TARSKI:def 3;
the InternalRel of G is_symmetric_in the carrier of G by NECKLACE:def 4;
then [b,x] in the InternalRel of G by A6, A13, A21, A32, A33, RELAT_2:def 3;
hence ex b being Element of R1 st [b,x] in the InternalRel of G ; :: thesis: verum
end;
end;
end;