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

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_{1}[ 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_{1}[ len p]
by A8, A10, CARD_1:27, FINSEQ_3:25, FINSEQ_5:6;

then A12: ex k being Nat st S_{1}[k]
;

ex n0 being Nat st

( S_{1}[n0] & ( for n being Nat st S_{1}[n] holds

n >= n0 ) ) from NAT_1:sch 5(A12);

then consider n0 being Element of NAT such that

A13: S_{1}[n0]
and

A14: for n being Nat st S_{1}[n] holds

n >= n0 ;

n0 <> 0

A15: n0 = k0 + 1 by NAT_1:6;

A16: n0 <> 1

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

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

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

reconsider A = the carrier of (subrelstr (([#] G) \ {x})) as Subset of G by YELLOW_0:def 15;
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;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

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

p . k in the carrier of R1 ) );

S

then A12: ex k being Nat st S

ex n0 being Nat st

( S

n >= n0 ) ) from NAT_1:sch 5(A12);

then consider n0 being Element of NAT such that

A13: S

A14: for n being Nat st S

n >= n0 ;

n0 <> 0

proof

then consider k0 being Nat such that
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 0 in Seg (len p) by A13, FINSEQ_1:def 3;

hence contradiction by FINSEQ_1:1; :: thesis: verum

A15: n0 = k0 + 1 by NAT_1:6;

A16: n0 <> 1

proof

A17:
k0 >= 1
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;then not x in {x} by A5, A4, A9, A13, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

proof

n0 in Seg (len p)
by A13, FINSEQ_1:def 3;
assume
not k0 >= 1
; :: thesis: contradiction

then k0 = 0 by NAT_1:25;

hence contradiction by A15, A16; :: thesis: verum

end;then k0 = 0 by NAT_1:25;

hence contradiction by A15, A16; :: thesis: verum

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

A24:
the carrier of G = the carrier of (subrelstr (([#] G) \ {x})) \/ {x}
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 hence contradiction by A13, A22, A23; :: thesis: verum

end;( 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 hence contradiction by A13, A22, A23; :: thesis: verum

proof

k0 <= n0
by A15, XREAL_1:29;
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

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

end;proof

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 )
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;assume A25: a in the carrier of G ; :: thesis: a in the carrier of (subrelstr (([#] G) \ {x})) \/ {x}

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

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
end;

per cases
( p . k0 in the carrier of (subrelstr (([#] G) \ {x})) or p . k0 in {x} )
by A29, A24, XBOOLE_0:def 3;

end;

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}))

end;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

hence
ex b being Element of R1 st [b,x] in the InternalRel of G
by A31, YELLOW_0:def 14; :: thesis: verum
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;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

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;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