let G be non empty symmetric RelStr ; 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; 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 ; ( 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
; 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
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
then consider k0 being Nat such that
A15:
n0 = k0 + 1
by NAT_1:6;
A16:
n0 <> 1
A17:
k0 >= 1
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 )
;
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
hence
contradiction
by A13, A22, A23;
verum
end;
A24:
the carrier of G = the carrier of (subrelstr (([#] G) \ {x})) \/ {x}
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
verumproof
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}))
;
ex b being Element of R1 st [b,x] in the InternalRel of Gset 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}))
hence
ex
b being
Element of
R1 st
[b,x] in the
InternalRel of
G
by A31, YELLOW_0:def 14;
verum end; end;
end;