let G be non empty symmetric irreflexive 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) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

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) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected implies G embeds Necklace 4 )

assume that

A1: the carrier of R1 misses the carrier of R2 and

A2: subrelstr (([#] G) \ {x}) = union_of (R1,R2) and

A3: not G is trivial and

A4: G is path-connected and

A5: ComplRelStr G is path-connected ; :: thesis: G embeds Necklace 4

consider a being Element of R1 such that

A6: [a,x] in the InternalRel of G by A1, A2, A4, Th37;

set A = the carrier of G \ {x};

set X = {x};

reconsider A = the carrier of G \ {x} as Subset of G ;

set R = subrelstr A;

reconsider R = subrelstr A as non empty symmetric irreflexive RelStr by A3, YELLOW_0:def 15;

( R = subrelstr (([#] G) \ {x}) & R = union_of (R2,R1) ) by A2, Th8;

then consider b being Element of R2 such that

A7: [b,x] in the InternalRel of G by A1, A4, Th37;

reconsider X1 = { y where y is Element of R1 : [y,x] in the InternalRel of G } , Y1 = { y where y is Element of R1 : not [y,x] in the InternalRel of G } , X2 = { y where y is Element of R2 : [y,x] in the InternalRel of G } , Y2 = { y where y is Element of R2 : not [y,x] in the InternalRel of G } as set ;

reconsider X = {x} as Subset of G ;

set H = subrelstr X;

A8: X1 misses Y1

A11: the carrier of R1 = X1 \/ Y1

A18: b in X2 by A7;

A19: the carrier of G = the carrier of R \/ {x}

for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

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) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected implies G embeds Necklace 4 )

assume that

A1: the carrier of R1 misses the carrier of R2 and

A2: subrelstr (([#] G) \ {x}) = union_of (R1,R2) and

A3: not G is trivial and

A4: G is path-connected and

A5: ComplRelStr G is path-connected ; :: thesis: G embeds Necklace 4

consider a being Element of R1 such that

A6: [a,x] in the InternalRel of G by A1, A2, A4, Th37;

set A = the carrier of G \ {x};

set X = {x};

reconsider A = the carrier of G \ {x} as Subset of G ;

set R = subrelstr A;

reconsider R = subrelstr A as non empty symmetric irreflexive RelStr by A3, YELLOW_0:def 15;

( R = subrelstr (([#] G) \ {x}) & R = union_of (R2,R1) ) by A2, Th8;

then consider b being Element of R2 such that

A7: [b,x] in the InternalRel of G by A1, A4, Th37;

reconsider X1 = { y where y is Element of R1 : [y,x] in the InternalRel of G } , Y1 = { y where y is Element of R1 : not [y,x] in the InternalRel of G } , X2 = { y where y is Element of R2 : [y,x] in the InternalRel of G } , Y2 = { y where y is Element of R2 : not [y,x] in the InternalRel of G } as set ;

reconsider X = {x} as Subset of G ;

set H = subrelstr X;

A8: X1 misses Y1

proof

A10:
a in X1
by A6;
assume
not X1 misses Y1
; :: thesis: contradiction

then consider a being object such that

A9: ( a in X1 & a in Y1 ) by XBOOLE_0:3;

( ex y1 being Element of R1 st

( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( y2 = a & not [y2,x] in the InternalRel of G ) ) by A9;

hence contradiction ; :: thesis: verum

end;then consider a being object such that

A9: ( a in X1 & a in Y1 ) by XBOOLE_0:3;

( ex y1 being Element of R1 st

( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( y2 = a & not [y2,x] in the InternalRel of G ) ) by A9;

hence contradiction ; :: thesis: verum

A11: the carrier of R1 = X1 \/ Y1

proof

A14:
X2 misses Y2
thus
the carrier of R1 c= X1 \/ Y1
:: according to XBOOLE_0:def 10 :: thesis: X1 \/ Y1 c= the carrier of R1

assume A13: a in X1 \/ Y1 ; :: thesis: a in the carrier of R1

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X1 \/ Y1 or a in the carrier of R1 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R1 or a in X1 \/ Y1 )

assume A12: a in the carrier of R1 ; :: thesis: a in X1 \/ Y1

end;assume A12: a in the carrier of R1 ; :: thesis: a in X1 \/ Y1

per cases
( [a,x] in the InternalRel of G or not [a,x] in the InternalRel of G )
;

end;

assume A13: a in X1 \/ Y1 ; :: thesis: a in the carrier of R1

per cases
( a in X1 or a in Y1 )
by A13, XBOOLE_0:def 3;

end;

suppose
a in X1
; :: thesis: a in the carrier of R1

then
ex y being Element of R1 st

( a = y & [y,x] in the InternalRel of G ) ;

hence a in the carrier of R1 ; :: thesis: verum

end;( a = y & [y,x] in the InternalRel of G ) ;

hence a in the carrier of R1 ; :: thesis: verum

suppose
a in Y1
; :: thesis: a in the carrier of R1

then
ex y being Element of R1 st

( a = y & not [y,x] in the InternalRel of G ) ;

hence a in the carrier of R1 ; :: thesis: verum

end;( a = y & not [y,x] in the InternalRel of G ) ;

hence a in the carrier of R1 ; :: thesis: verum

proof

A16:
the carrier of (subrelstr X) misses the carrier of R
assume
not X2 misses Y2
; :: thesis: contradiction

then consider a being object such that

A15: ( a in X2 & a in Y2 ) by XBOOLE_0:3;

( ex y1 being Element of R2 st

( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( y2 = a & not [y2,x] in the InternalRel of G ) ) by A15;

hence contradiction ; :: thesis: verum

end;then consider a being object such that

A15: ( a in X2 & a in Y2 ) by XBOOLE_0:3;

( ex y1 being Element of R2 st

( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( y2 = a & not [y2,x] in the InternalRel of G ) ) by A15;

hence contradiction ; :: thesis: verum

proof

reconsider H = subrelstr X as non empty symmetric irreflexive RelStr by YELLOW_0:def 15;
assume
not the carrier of (subrelstr X) misses the carrier of R
; :: thesis: contradiction

then the carrier of (subrelstr X) /\ the carrier of R <> {} ;

then X /\ the carrier of R <> {} by YELLOW_0:def 15;

then X /\ A <> {} by YELLOW_0:def 15;

then consider a being object such that

A17: a in X /\ A by XBOOLE_0:def 1;

( a in X & a in A ) by A17, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;then the carrier of (subrelstr X) /\ the carrier of R <> {} ;

then X /\ the carrier of R <> {} by YELLOW_0:def 15;

then X /\ A <> {} by YELLOW_0:def 15;

then consider a being object such that

A17: a in X /\ A by XBOOLE_0:def 1;

( a in X & a in A ) by A17, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

A18: b in X2 by A7;

A19: the carrier of G = the carrier of R \/ {x}

proof

A22:
the carrier of R2 = X2 \/ Y2
thus
the carrier of G c= the carrier of R \/ {x}
:: according to XBOOLE_0:def 10 :: thesis: the carrier of R \/ {x} c= the carrier of G

assume A21: a in the carrier of R \/ {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 R \/ {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 R \/ {x} )

assume A20: a in the carrier of G ; :: thesis: a in the carrier of R \/ {x}

end;assume A20: a in the carrier of G ; :: thesis: a in the carrier of R \/ {x}

per cases
( a = x or a <> x )
;

end;

suppose
a = x
; :: thesis: a in the carrier of R \/ {x}

then
a in {x}
by TARSKI:def 1;

hence a in the carrier of R \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;hence a in the carrier of R \/ {x} by XBOOLE_0:def 3; :: thesis: verum

suppose
a <> x
; :: thesis: a in the carrier of R \/ {x}

then
not a in {x}
by TARSKI:def 1;

then a in the carrier of G \ {x} by A20, XBOOLE_0:def 5;

then a in the carrier of R by YELLOW_0:def 15;

hence a in the carrier of R \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;then a in the carrier of G \ {x} by A20, XBOOLE_0:def 5;

then a in the carrier of R by YELLOW_0:def 15;

hence a in the carrier of R \/ {x} by XBOOLE_0:def 3; :: thesis: verum

assume A21: a in the carrier of R \/ {x} ; :: thesis: a in the carrier of G

proof

A25:
not Y1 \/ Y2 is empty
thus
the carrier of R2 c= X2 \/ Y2
:: according to XBOOLE_0:def 10 :: thesis: X2 \/ Y2 c= the carrier of R2

assume A24: a in X2 \/ Y2 ; :: thesis: a in the carrier of R2

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X2 \/ Y2 or a in the carrier of R2 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R2 or a in X2 \/ Y2 )

assume A23: a in the carrier of R2 ; :: thesis: a in X2 \/ Y2

end;assume A23: a in the carrier of R2 ; :: thesis: a in X2 \/ Y2

per cases
( [a,x] in the InternalRel of G or not [a,x] in the InternalRel of G )
;

end;

assume A24: a in X2 \/ Y2 ; :: thesis: a in the carrier of R2

per cases
( a in X2 or a in Y2 )
by A24, XBOOLE_0:def 3;

end;

suppose
a in X2
; :: thesis: a in the carrier of R2

then
ex y being Element of R2 st

( a = y & [y,x] in the InternalRel of G ) ;

hence a in the carrier of R2 ; :: thesis: verum

end;( a = y & [y,x] in the InternalRel of G ) ;

hence a in the carrier of R2 ; :: thesis: verum

suppose
a in Y2
; :: thesis: a in the carrier of R2

then
ex y being Element of R2 st

( a = y & not [y,x] in the InternalRel of G ) ;

hence a in the carrier of R2 ; :: thesis: verum

end;( a = y & not [y,x] in the InternalRel of G ) ;

hence a in the carrier of R2 ; :: thesis: verum

proof

thus
G embeds Necklace 4
:: thesis: verum
assume A26:
Y1 \/ Y2 is empty
; :: thesis: contradiction

then A27: Y2 is empty ;

A28: Y1 is empty by A26;

A29: for a being Element of R holds [a,x] in the InternalRel of G

end;then A27: Y2 is empty ;

A28: Y1 is empty by A26;

A29: for a being Element of R holds [a,x] in the InternalRel of G

proof

not ComplRelStr G is path-connected
let a be Element of R; :: thesis: [a,x] in the InternalRel of G

A30: the carrier of R = the carrier of R1 \/ the carrier of R2 by A2, NECKLA_2:def 2;

end;A30: the carrier of R = the carrier of R1 \/ the carrier of R2 by A2, NECKLA_2:def 2;

per cases
( a in the carrier of R1 or a in the carrier of R2 )
by A30, XBOOLE_0:def 3;

end;

suppose
a in the carrier of R1
; :: thesis: [a,x] in the InternalRel of G

then
ex y being Element of R1 st

( a = y & [y,x] in the InternalRel of G ) by A11, A28;

hence [a,x] in the InternalRel of G ; :: thesis: verum

end;( a = y & [y,x] in the InternalRel of G ) by A11, A28;

hence [a,x] in the InternalRel of G ; :: thesis: verum

suppose
a in the carrier of R2
; :: thesis: [a,x] in the InternalRel of G

then
ex y being Element of R2 st

( a = y & [y,x] in the InternalRel of G ) by A22, A27;

hence [a,x] in the InternalRel of G ; :: thesis: verum

end;( a = y & [y,x] in the InternalRel of G ) by A22, A27;

hence [a,x] in the InternalRel of G ; :: thesis: verum

proof

hence
contradiction
by A5; :: thesis: verum
A31:
a <> x

then A33: a in the carrier of R by A2, NECKLA_2:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then A34: a is Element of (ComplRelStr G) by A33, NECKLACE:def 8;

A35: x is Element of (ComplRelStr G) by NECKLACE:def 8;

assume ComplRelStr G is path-connected ; :: thesis: contradiction

then the InternalRel of (ComplRelStr G) reduces x,a by A31, A34, A35;

then consider p being FinSequence such that

A36: len p > 0 and

A37: p . 1 = x and

A38: p . (len p) = a and

A39: for i being Nat st i in dom p & i + 1 in dom p holds

[(p . i),(p . (i + 1))] in the InternalRel of (ComplRelStr G) by REWRITE1:11;

A40: 0 + 1 <= len p by A36, NAT_1:13;

then len p > 1 by A31, A37, A38, XXREAL_0:1;

then 1 + 1 <= len p by NAT_1:13;

then A41: 2 in dom p by FINSEQ_3:25;

1 in dom p by A40, FINSEQ_3:25;

then A42: [(p . 1),(p . (1 + 1))] in the InternalRel of (ComplRelStr G) by A39, A41;

A43: p . 2 <> x

then A45: p . 2 in the carrier of G by NECKLACE:def 8;

p . 2 in the carrier of R

A47: the InternalRel of (ComplRelStr G) is_symmetric_in the carrier of (ComplRelStr G) by NECKLACE:def 3;

( p . 1 in the carrier of (ComplRelStr G) & p . (1 + 1) in the carrier of (ComplRelStr G) ) by A42, ZFMISC_1:87;

then [(p . (1 + 1)),(p . 1)] in the InternalRel of (ComplRelStr G) by A42, A47;

then [(p . 2),x] in the InternalRel of (ComplRelStr G) /\ the InternalRel of G by A37, A46, XBOOLE_0:def 4;

then the InternalRel of (ComplRelStr G) meets the InternalRel of G ;

hence contradiction by Th12; :: thesis: verum

end;proof

a in the carrier of R1 \/ the carrier of R2
by XBOOLE_0:def 3;
assume
not a <> x
; :: thesis: contradiction

then x in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A32: x in the carrier of R by A2, NECKLA_2:def 2;

x in {x} by TARSKI:def 1;

then x in the carrier of H by YELLOW_0:def 15;

then x in the carrier of R /\ the carrier of H by A32, XBOOLE_0:def 4;

hence contradiction by A16; :: thesis: verum

end;then x in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A32: x in the carrier of R by A2, NECKLA_2:def 2;

x in {x} by TARSKI:def 1;

then x in the carrier of H by YELLOW_0:def 15;

then x in the carrier of R /\ the carrier of H by A32, XBOOLE_0:def 4;

hence contradiction by A16; :: thesis: verum

then A33: a in the carrier of R by A2, NECKLA_2:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then A34: a is Element of (ComplRelStr G) by A33, NECKLACE:def 8;

A35: x is Element of (ComplRelStr G) by NECKLACE:def 8;

assume ComplRelStr G is path-connected ; :: thesis: contradiction

then the InternalRel of (ComplRelStr G) reduces x,a by A31, A34, A35;

then consider p being FinSequence such that

A36: len p > 0 and

A37: p . 1 = x and

A38: p . (len p) = a and

A39: for i being Nat st i in dom p & i + 1 in dom p holds

[(p . i),(p . (i + 1))] in the InternalRel of (ComplRelStr G) by REWRITE1:11;

A40: 0 + 1 <= len p by A36, NAT_1:13;

then len p > 1 by A31, A37, A38, XXREAL_0:1;

then 1 + 1 <= len p by NAT_1:13;

then A41: 2 in dom p by FINSEQ_3:25;

1 in dom p by A40, FINSEQ_3:25;

then A42: [(p . 1),(p . (1 + 1))] in the InternalRel of (ComplRelStr G) by A39, A41;

A43: p . 2 <> x

proof

p . 2 in the carrier of (ComplRelStr G)
by A42, ZFMISC_1:87;
A44:
[x,x] in id the carrier of G
by RELAT_1:def 10;

assume not p . 2 <> x ; :: thesis: contradiction

then [x,x] in the InternalRel of (ComplRelStr G) /\ (id the carrier of G) by A37, A42, A44, XBOOLE_0:def 4;

then the InternalRel of (ComplRelStr G) meets id the carrier of G ;

hence contradiction by Th13; :: thesis: verum

end;assume not p . 2 <> x ; :: thesis: contradiction

then [x,x] in the InternalRel of (ComplRelStr G) /\ (id the carrier of G) by A37, A42, A44, XBOOLE_0:def 4;

then the InternalRel of (ComplRelStr G) meets id the carrier of G ;

hence contradiction by Th13; :: thesis: verum

then A45: p . 2 in the carrier of G by NECKLACE:def 8;

p . 2 in the carrier of R

proof

then A46:
[(p . 2),x] in the InternalRel of G
by A29;
assume
not p . 2 in the carrier of R
; :: thesis: contradiction

then p . 2 in {x} by A19, A45, XBOOLE_0:def 3;

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

end;then p . 2 in {x} by A19, A45, XBOOLE_0:def 3;

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

A47: the InternalRel of (ComplRelStr G) is_symmetric_in the carrier of (ComplRelStr G) by NECKLACE:def 3;

( p . 1 in the carrier of (ComplRelStr G) & p . (1 + 1) in the carrier of (ComplRelStr G) ) by A42, ZFMISC_1:87;

then [(p . (1 + 1)),(p . 1)] in the InternalRel of (ComplRelStr G) by A42, A47;

then [(p . 2),x] in the InternalRel of (ComplRelStr G) /\ the InternalRel of G by A37, A46, XBOOLE_0:def 4;

then the InternalRel of (ComplRelStr G) meets the InternalRel of G ;

hence contradiction by Th12; :: thesis: verum

proof
end;

per cases
( not Y1 is empty or not Y2 is empty )
by A25;

end;

suppose A48:
not Y1 is empty
; :: thesis: G embeds Necklace 4

ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G

A82: [u,v] in the InternalRel of G ;

set w = the Element of X2;

the Element of X2 in X2 by A18;

then A83: ex y being Element of R2 st

( y = the Element of X2 & [y,x] in the InternalRel of G ) ;

set Z = {u,v,x, the Element of X2};

{u,v,x, the Element of X2} c= the carrier of G

reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;

A88: the Element of X2 in X2 by A18;

reconsider w = the Element of X2 as Element of G by A83, ZFMISC_1:87;

A89: v in X1 by A10;

A90: [x,w] in the InternalRel of G

reconsider u = u, v = v as Element of G by A82, ZFMISC_1:87;

A92: [v,x] in the InternalRel of G

then A114: subrelstr Z embeds Necklace 4 by A82, A92, A90, A95, A102, A96, Th38;

G embeds Necklace 4

end;proof

then consider u being Element of Y1, v being Element of X1 such that
set b = the Element of Y1;

a in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A49: a in the carrier of R by A2, NECKLA_2:def 2;

the Element of Y1 in Y1 by A48;

then ex y being Element of R1 st

( y = the Element of Y1 & not [y,x] in the InternalRel of G ) ;

then the Element of Y1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A50: the Element of Y1 in the carrier of R by A2, NECKLA_2:def 2;

A51: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then reconsider a = a as Element of G by A49;

reconsider b = the Element of Y1 as Element of G by A51, A50;

a <> b

then consider p being FinSequence such that

A53: len p > 0 and

A54: p . 1 = a and

A55: p . (len p) = b and

A56: 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 Y1 & $1 in dom p & ( for k being Nat st k > $1 & k in dom p holds

p . k in Y1 ) );

for k being Nat st k > len p & k in dom p holds

p . k in Y1_{1}[ len p]
by A48, A53, A55, CARD_1:27, FINSEQ_5:6;

then A58: 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(A58);

then consider n0 being Nat such that

A59: S_{1}[n0]
and

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

n >= n0 ;

n0 <> 0

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

A62: n0 <> 1

then ( k0 <= k0 + 1 & n0 <= len p ) by FINSEQ_1:1, XREAL_1:29;

then A65: k0 <= len p by A61, XXREAL_0:2;

then A66: k0 in dom p by A64, FINSEQ_3:25;

then A67: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A56, A59, A61;

then A68: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by NECKLACE:def 3, ZFMISC_1:87;

p . n0 in the carrier of G by A61, A67, ZFMISC_1:87;

then A69: [(p . n0),(p . k0)] in the InternalRel of G by A61, A67, A68;

A70: for k being Nat st k > k0 & k in dom p holds

p . k in Y1

then A74: not S_{1}[k0]
by A60;

p . k0 in the carrier of G by A67, ZFMISC_1:87;

then ( p . k0 in the carrier of R or p . k0 in {x} ) by A19, XBOOLE_0:def 3;

then A75: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by A2, NECKLA_2:def 2;

thus ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G :: thesis: verum

end;a in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A49: a in the carrier of R by A2, NECKLA_2:def 2;

the Element of Y1 in Y1 by A48;

then ex y being Element of R1 st

( y = the Element of Y1 & not [y,x] in the InternalRel of G ) ;

then the Element of Y1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A50: the Element of Y1 in the carrier of R by A2, NECKLA_2:def 2;

A51: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then reconsider a = a as Element of G by A49;

reconsider b = the Element of Y1 as Element of G by A51, A50;

a <> b

proof

then
the InternalRel of G reduces a,b
by A4;
assume A52:
not a <> b
; :: thesis: contradiction

a in X1 by A6;

then a in X1 /\ Y1 by A48, A52, XBOOLE_0:def 4;

hence contradiction by A8; :: thesis: verum

end;a in X1 by A6;

then a in X1 /\ Y1 by A48, A52, XBOOLE_0:def 4;

hence contradiction by A8; :: thesis: verum

then consider p being FinSequence such that

A53: len p > 0 and

A54: p . 1 = a and

A55: p . (len p) = b and

A56: 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 Y1 ) );

for k being Nat st k > len p & k in dom p holds

p . k in Y1

proof

then
S
let k be Nat; :: thesis: ( k > len p & k in dom p implies p . k in Y1 )

assume A57: k > len p ; :: thesis: ( not k in dom p or p . k in Y1 )

assume k in dom p ; :: thesis: p . k in Y1

then k in Seg (len p) by FINSEQ_1:def 3;

hence p . k in Y1 by A57, FINSEQ_1:1; :: thesis: verum

end;assume A57: k > len p ; :: thesis: ( not k in dom p or p . k in Y1 )

assume k in dom p ; :: thesis: p . k in Y1

then k in Seg (len p) by FINSEQ_1:def 3;

hence p . k in Y1 by A57, FINSEQ_1:1; :: thesis: verum

then A58: ex k being Nat st S

ex n0 being Nat st

( S

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

then consider n0 being Nat such that

A59: S

A60: 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 A59, FINSEQ_1:def 3;

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

end;then 0 in Seg (len p) by A59, FINSEQ_1:def 3;

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

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

A62: n0 <> 1

proof

A64:
k0 >= 1
assume A63:
not n0 <> 1
; :: thesis: contradiction

a in X1 by A6;

then not X1 /\ Y1 is empty by A54, A59, A63, XBOOLE_0:def 4;

hence contradiction by A8; :: thesis: verum

end;a in X1 by A6;

then not X1 /\ Y1 is empty by A54, A59, A63, XBOOLE_0:def 4;

hence contradiction by A8; :: thesis: verum

proof

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

then k0 = 0 by NAT_1:25;

hence contradiction by A61, A62; :: thesis: verum

end;then k0 = 0 by NAT_1:25;

hence contradiction by A61, A62; :: thesis: verum

then ( k0 <= k0 + 1 & n0 <= len p ) by FINSEQ_1:1, XREAL_1:29;

then A65: k0 <= len p by A61, XXREAL_0:2;

then A66: k0 in dom p by A64, FINSEQ_3:25;

then A67: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A56, A59, A61;

then A68: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by NECKLACE:def 3, ZFMISC_1:87;

p . n0 in the carrier of G by A61, A67, ZFMISC_1:87;

then A69: [(p . n0),(p . k0)] in the InternalRel of G by A61, A67, A68;

A70: for k being Nat st k > k0 & k in dom p holds

p . k in Y1

proof

k0 < n0
by A61, NAT_1:13;
assume
ex k being Nat st

( k > k0 & k in dom p & not p . k in Y1 ) ; :: thesis: contradiction

then consider k being Nat such that

A71: k > k0 and

A72: k in dom p and

A73: not p . k in Y1 ;

k > n0 hence contradiction by A59, A72, A73; :: thesis: verum

end;( k > k0 & k in dom p & not p . k in Y1 ) ; :: thesis: contradiction

then consider k being Nat such that

A71: k > k0 and

A72: k in dom p and

A73: not p . k in Y1 ;

k > n0 hence contradiction by A59, A72, A73; :: thesis: verum

then A74: not S

p . k0 in the carrier of G by A67, ZFMISC_1:87;

then ( p . k0 in the carrier of R or p . k0 in {x} ) by A19, XBOOLE_0:def 3;

then A75: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by A2, NECKLA_2:def 2;

thus ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G :: thesis: verum

proof
end;

per cases
( ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) or ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) or ( p . k0 in {x} & p . n0 in the carrier of G ) )
by A61, A67, A75, XBOOLE_0:def 3, ZFMISC_1:87;

end;

suppose A76:
( p . k0 in the carrier of R1 & p . n0 in the carrier of G )
; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G

then reconsider m = p . k0 as Element of X1 by A11, A64, A65, A74, A70, FINSEQ_3:25, XBOOLE_0:def 3;

m in the carrier of R1 \/ the carrier of R2 by A76, XBOOLE_0:def 3;

then A77: m in the carrier of R by A2, NECKLA_2:def 2;

reconsider l = p . n0 as Element of Y1 by A59;

A78: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

l in the carrier of R1 by A11, A59, XBOOLE_0:def 3;

then l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A79: l in the carrier of R by A2, NECKLA_2:def 2;

( [m,l] in the InternalRel of G & the InternalRel of G is_symmetric_in the carrier of G ) by A56, A59, A61, A66, NECKLACE:def 3;

then [l,m] in the InternalRel of G by A79, A77, A78;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G ; :: thesis: verum

end;m in the carrier of R1 \/ the carrier of R2 by A76, XBOOLE_0:def 3;

then A77: m in the carrier of R by A2, NECKLA_2:def 2;

reconsider l = p . n0 as Element of Y1 by A59;

A78: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

l in the carrier of R1 by A11, A59, XBOOLE_0:def 3;

then l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A79: l in the carrier of R by A2, NECKLA_2:def 2;

( [m,l] in the InternalRel of G & the InternalRel of G is_symmetric_in the carrier of G ) by A56, A59, A61, A66, NECKLACE:def 3;

then [l,m] in the InternalRel of G by A79, A77, A78;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G ; :: thesis: verum

suppose
( p . k0 in the carrier of R2 & p . n0 in the carrier of G )
; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G

then reconsider m = p . k0 as Element of R2 ;

reconsider l = p . n0 as Element of R1 by A11, A59, XBOOLE_0:def 3;

m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A80: m in the carrier of R by A2, NECKLA_2:def 2;

l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then l in the carrier of R by A2, NECKLA_2:def 2;

then [l,m] in [: the carrier of R, the carrier of R:] by A80, ZFMISC_1:87;

then [l,m] in the InternalRel of G |_2 the carrier of R by A69, XBOOLE_0:def 4;

then [l,m] in the InternalRel of R by YELLOW_0:def 14;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by A1, A2, Th35; :: thesis: verum

end;reconsider l = p . n0 as Element of R1 by A11, A59, XBOOLE_0:def 3;

m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A80: m in the carrier of R by A2, NECKLA_2:def 2;

l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then l in the carrier of R by A2, NECKLA_2:def 2;

then [l,m] in [: the carrier of R, the carrier of R:] by A80, ZFMISC_1:87;

then [l,m] in the InternalRel of G |_2 the carrier of R by A69, XBOOLE_0:def 4;

then [l,m] in the InternalRel of R by YELLOW_0:def 14;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by A1, A2, Th35; :: thesis: verum

suppose A81:
( p . k0 in {x} & p . n0 in the carrier of G )
; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G

ex y1 being Element of R1 st

( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A59;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by A69, A81, TARSKI:def 1; :: thesis: verum

end;( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A59;

hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by A69, A81, TARSKI:def 1; :: thesis: verum

A82: [u,v] in the InternalRel of G ;

set w = the Element of X2;

the Element of X2 in X2 by A18;

then A83: ex y being Element of R2 st

( y = the Element of X2 & [y,x] in the InternalRel of G ) ;

set Z = {u,v,x, the Element of X2};

{u,v,x, the Element of X2} c= the carrier of G

proof

then reconsider Z = {u,v,x, the Element of X2} as Subset of G ;
the Element of X2 in X2
by A18;

then ex y2 being Element of R2 st

( y2 = the Element of X2 & [y2,x] in the InternalRel of G ) ;

then the Element of X2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A84: the Element of X2 in the carrier of R by A2, NECKLA_2:def 2;

v in X1 by A10;

then ex y1 being Element of R1 st

( y1 = v & [y1,x] in the InternalRel of G ) ;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A85: v in the carrier of R by A2, NECKLA_2:def 2;

u in the carrier of R1 by A11, A48, XBOOLE_0:def 3;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A86: u in the carrier of R by A2, NECKLA_2:def 2;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X2} or q in the carrier of G )

assume q in {u,v,x, the Element of X2} ; :: thesis: q in the carrier of G

then A87: ( q = u or q = v or q = x or q = the Element of X2 ) by ENUMSET1:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

hence q in the carrier of G by A87, A86, A85, A84; :: thesis: verum

end;then ex y2 being Element of R2 st

( y2 = the Element of X2 & [y2,x] in the InternalRel of G ) ;

then the Element of X2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A84: the Element of X2 in the carrier of R by A2, NECKLA_2:def 2;

v in X1 by A10;

then ex y1 being Element of R1 st

( y1 = v & [y1,x] in the InternalRel of G ) ;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A85: v in the carrier of R by A2, NECKLA_2:def 2;

u in the carrier of R1 by A11, A48, XBOOLE_0:def 3;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A86: u in the carrier of R by A2, NECKLA_2:def 2;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X2} or q in the carrier of G )

assume q in {u,v,x, the Element of X2} ; :: thesis: q in the carrier of G

then A87: ( q = u or q = v or q = x or q = the Element of X2 ) by ENUMSET1:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

hence q in the carrier of G by A87, A86, A85, A84; :: thesis: verum

reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;

A88: the Element of X2 in X2 by A18;

reconsider w = the Element of X2 as Element of G by A83, ZFMISC_1:87;

A89: v in X1 by A10;

A90: [x,w] in the InternalRel of G

proof

A91:
u in Y1
by A48;
( ex y1 being Element of R2 st

( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by A88, NECKLACE:def 3;

hence [x,w] in the InternalRel of G ; :: thesis: verum

end;( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by A88, NECKLACE:def 3;

hence [x,w] in the InternalRel of G ; :: thesis: verum

reconsider u = u, v = v as Element of G by A82, ZFMISC_1:87;

A92: [v,x] in the InternalRel of G

proof

A93:
w <> u
ex y1 being Element of R1 st

( v = y1 & [y1,x] in the InternalRel of G ) by A89;

hence [v,x] in the InternalRel of G ; :: thesis: verum

end;( v = y1 & [y1,x] in the InternalRel of G ) by A89;

hence [v,x] in the InternalRel of G ; :: thesis: verum

proof

A95:
not [u,x] in the InternalRel of G
assume A94:
not w <> u
; :: thesis: contradiction

( ex y1 being Element of R2 st

( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( u = y2 & not [y2,x] in the InternalRel of G ) ) by A91, A88;

hence contradiction by A94; :: thesis: verum

end;( ex y1 being Element of R2 st

( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( u = y2 & not [y2,x] in the InternalRel of G ) ) by A91, A88;

hence contradiction by A94; :: thesis: verum

proof

A96:
not [v,w] in the InternalRel of G
ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

hence not [u,x] in the InternalRel of G ; :: thesis: verum

end;( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

hence not [u,x] in the InternalRel of G ; :: thesis: verum

proof

A100:
w <> x
A97:
ex y2 being Element of R2 st

( w = y2 & [y2,x] in the InternalRel of G ) by A88;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A98: ex y1 being Element of R1 st

( v = y1 & [y1,x] in the InternalRel of G ) by A89;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider v = v as Element of R by A2, NECKLA_2:def 2;

assume [v,w] in the InternalRel of G ; :: thesis: contradiction

then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [v,w] in the InternalRel of R by YELLOW_0:def 14;

then A99: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

end;( w = y2 & [y2,x] in the InternalRel of G ) by A88;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A98: ex y1 being Element of R1 st

( v = y1 & [y1,x] in the InternalRel of G ) by A89;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider v = v as Element of R by A2, NECKLA_2:def 2;

assume [v,w] in the InternalRel of G ; :: thesis: contradiction

then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [v,w] in the InternalRel of R by YELLOW_0:def 14;

then A99: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

per cases
( [v,w] in the InternalRel of R1 or [v,w] in the InternalRel of R2 )
by A99, XBOOLE_0:def 3;

end;

suppose
[v,w] in the InternalRel of R1
; :: thesis: contradiction

then
w in the carrier of R1
by ZFMISC_1:87;

then w in the carrier of R1 /\ the carrier of R2 by A97, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then w in the carrier of R1 /\ the carrier of R2 by A97, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

suppose
[v,w] in the InternalRel of R2
; :: thesis: contradiction

then
v in the carrier of R2
by ZFMISC_1:87;

then v in the carrier of R1 /\ the carrier of R2 by A98, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then v in the carrier of R1 /\ the carrier of R2 by A98, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

A102:
not [u,w] in the InternalRel of G
assume A101:
not w <> x
; :: thesis: contradiction

ex y1 being Element of R2 st

( w = y1 & [y1,x] in the InternalRel of G ) by A88;

then x in the carrier of R1 \/ the carrier of R2 by A101, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R2 st

( w = y1 & [y1,x] in the InternalRel of G ) by A88;

then x in the carrier of R1 \/ the carrier of R2 by A101, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

A106:
x <> u
A103:
ex y2 being Element of R2 st

( w = y2 & [y2,x] in the InternalRel of G ) by A88;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A104: ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider u = u as Element of R by A2, NECKLA_2:def 2;

assume [u,w] in the InternalRel of G ; :: thesis: contradiction

then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [u,w] in the InternalRel of R by YELLOW_0:def 14;

then A105: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

end;( w = y2 & [y2,x] in the InternalRel of G ) by A88;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A104: ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider u = u as Element of R by A2, NECKLA_2:def 2;

assume [u,w] in the InternalRel of G ; :: thesis: contradiction

then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [u,w] in the InternalRel of R by YELLOW_0:def 14;

then A105: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

per cases
( [u,w] in the InternalRel of R1 or [u,w] in the InternalRel of R2 )
by A105, XBOOLE_0:def 3;

end;

suppose
[u,w] in the InternalRel of R1
; :: thesis: contradiction

then
w in the carrier of R1
by ZFMISC_1:87;

then w in the carrier of R1 /\ the carrier of R2 by A103, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then w in the carrier of R1 /\ the carrier of R2 by A103, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

suppose
[u,w] in the InternalRel of R2
; :: thesis: contradiction

then
u in the carrier of R2
by ZFMISC_1:87;

then u in the carrier of R1 /\ the carrier of R2 by A104, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then u in the carrier of R1 /\ the carrier of R2 by A104, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

A108:
w <> v
assume A107:
not x <> u
; :: thesis: contradiction

ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

then x in the carrier of R1 \/ the carrier of R2 by A107, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A91;

then x in the carrier of R1 \/ the carrier of R2 by A107, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

A111:
v <> x
consider y1 being Element of R2 such that

A109: w = y1 and

[y1,x] in the InternalRel of G by A88;

assume A110: not w <> v ; :: thesis: contradiction

ex y2 being Element of R1 st

( v = y2 & [y2,x] in the InternalRel of G ) by A89;

then y1 in the carrier of R1 /\ the carrier of R2 by A110, A109, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;A109: w = y1 and

[y1,x] in the InternalRel of G by A88;

assume A110: not w <> v ; :: thesis: contradiction

ex y2 being Element of R1 st

( v = y2 & [y2,x] in the InternalRel of G ) by A89;

then y1 in the carrier of R1 /\ the carrier of R2 by A110, A109, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

u <> v
assume A112:
not v <> x
; :: thesis: contradiction

ex y1 being Element of R1 st

( v = y1 & [y1,x] in the InternalRel of G ) by A89;

then x in the carrier of R1 \/ the carrier of R2 by A112, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R1 st

( v = y1 & [y1,x] in the InternalRel of G ) by A89;

then x in the carrier of R1 \/ the carrier of R2 by A112, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

then
u,v,x,w are_mutually_distinct
by A111, A106, A93, A108, A100, ZFMISC_1:def 6;
assume A113:
not u <> v
; :: thesis: contradiction

( ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( v = y2 & [y2,x] in the InternalRel of G ) ) by A91, A89;

hence contradiction by A113; :: thesis: verum

end;( ex y1 being Element of R1 st

( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st

( v = y2 & [y2,x] in the InternalRel of G ) ) by A91, A89;

hence contradiction by A113; :: thesis: verum

then A114: subrelstr Z embeds Necklace 4 by A82, A92, A90, A95, A102, A96, Th38;

G embeds Necklace 4

proof

hence
G embeds Necklace 4
; :: thesis: verum
assume
not G embeds Necklace 4
; :: thesis: contradiction

then G is N-free by NECKLA_2:def 1;

then H is N-free by Th23;

hence contradiction by A114, NECKLA_2:def 1; :: thesis: verum

end;then G is N-free by NECKLA_2:def 1;

then H is N-free by Th23;

hence contradiction by A114, NECKLA_2:def 1; :: thesis: verum

suppose A115:
not Y2 is empty
; :: thesis: G embeds Necklace 4

ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G

A146: [u,v] in the InternalRel of G ;

set w = the Element of X1;

the Element of X1 in X1 by A10;

then A147: ex y being Element of R1 st

( y = the Element of X1 & [y,x] in the InternalRel of G ) ;

set Z = {u,v,x, the Element of X1};

{u,v,x, the Element of X1} c= the carrier of G

reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;

A152: the Element of X1 in X1 by A10;

reconsider w = the Element of X1 as Element of G by A147, ZFMISC_1:87;

A153: v in X2 by A18;

A154: [x,w] in the InternalRel of G

reconsider u = u, v = v as Element of G by A146, ZFMISC_1:87;

A156: [v,x] in the InternalRel of G

then A178: subrelstr Z embeds Necklace 4 by A146, A156, A154, A159, A166, A160, Th38;

G embeds Necklace 4

end;proof

then consider u being Element of Y2, v being Element of X2 such that
set c = the Element of Y2;

b in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A116: b in the carrier of R by A2, NECKLA_2:def 2;

the Element of Y2 in Y2 by A115;

then ex y being Element of R2 st

( y = the Element of Y2 & not [y,x] in the InternalRel of G ) ;

then the Element of Y2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A117: the Element of Y2 in the carrier of R by A2, NECKLA_2:def 2;

A118: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then reconsider b = b as Element of G by A116;

reconsider c = the Element of Y2 as Element of G by A118, A117;

b <> c

then consider p being FinSequence such that

A119: len p > 0 and

A120: p . 1 = b and

A121: p . (len p) = c and

A122: 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 Y2 & $1 in dom p & ( for k being Nat st k > $1 & k in dom p holds

p . k in Y2 ) );

for k being Nat st k > len p & k in dom p holds

p . k in Y2_{1}[ len p]
by A115, A119, A121, CARD_1:27, FINSEQ_5:6;

then A124: 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(A124);

then consider n0 being Nat such that

A125: S_{1}[n0]
and

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

n >= n0 ;

n0 <> 0

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

A128: n0 <> 1

then ( k0 <= k0 + 1 & n0 <= len p ) by FINSEQ_1:1, XREAL_1:29;

then k0 <= len p by A127, XXREAL_0:2;

then A131: k0 in Seg (len p) by A130, FINSEQ_1:1;

then A132: k0 in dom p by FINSEQ_1:def 3;

then A133: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A122, A125, A127;

then A134: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by NECKLACE:def 3, ZFMISC_1:87;

p . n0 in the carrier of G by A127, A133, ZFMISC_1:87;

then A135: [(p . n0),(p . k0)] in the InternalRel of G by A127, A133, A134;

A136: for k being Nat st k > k0 & k in dom p holds

p . k in Y2

then A140: not S_{1}[k0]
by A126;

p . k0 in the carrier of G by A133, ZFMISC_1:87;

then ( p . k0 in the carrier of R or p . k0 in {x} ) by A19, XBOOLE_0:def 3;

then A141: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by A2, NECKLA_2:def 2;

thus ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G :: thesis: verum

end;b in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A116: b in the carrier of R by A2, NECKLA_2:def 2;

the Element of Y2 in Y2 by A115;

then ex y being Element of R2 st

( y = the Element of Y2 & not [y,x] in the InternalRel of G ) ;

then the Element of Y2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A117: the Element of Y2 in the carrier of R by A2, NECKLA_2:def 2;

A118: the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

then reconsider b = b as Element of G by A116;

reconsider c = the Element of Y2 as Element of G by A118, A117;

b <> c

proof

then
the InternalRel of G reduces b,c
by A4;
assume
not b <> c
; :: thesis: contradiction

then c in X2 by A7;

then c in X2 /\ Y2 by A115, XBOOLE_0:def 4;

hence contradiction by A14; :: thesis: verum

end;then c in X2 by A7;

then c in X2 /\ Y2 by A115, XBOOLE_0:def 4;

hence contradiction by A14; :: thesis: verum

then consider p being FinSequence such that

A119: len p > 0 and

A120: p . 1 = b and

A121: p . (len p) = c and

A122: 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 Y2 ) );

for k being Nat st k > len p & k in dom p holds

p . k in Y2

proof

then
S
let k be Nat; :: thesis: ( k > len p & k in dom p implies p . k in Y2 )

assume A123: k > len p ; :: thesis: ( not k in dom p or p . k in Y2 )

assume k in dom p ; :: thesis: p . k in Y2

then k in Seg (len p) by FINSEQ_1:def 3;

hence p . k in Y2 by A123, FINSEQ_1:1; :: thesis: verum

end;assume A123: k > len p ; :: thesis: ( not k in dom p or p . k in Y2 )

assume k in dom p ; :: thesis: p . k in Y2

then k in Seg (len p) by FINSEQ_1:def 3;

hence p . k in Y2 by A123, FINSEQ_1:1; :: thesis: verum

then A124: ex k being Nat st S

ex n0 being Nat st

( S

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

then consider n0 being Nat such that

A125: S

A126: 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 A125, FINSEQ_1:def 3;

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

end;then 0 in Seg (len p) by A125, FINSEQ_1:def 3;

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

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

A128: n0 <> 1

proof

A130:
k0 >= 1
assume A129:
not n0 <> 1
; :: thesis: contradiction

b in X2 by A7;

then not X2 /\ Y2 is empty by A120, A125, A129, XBOOLE_0:def 4;

hence contradiction by A14; :: thesis: verum

end;b in X2 by A7;

then not X2 /\ Y2 is empty by A120, A125, A129, XBOOLE_0:def 4;

hence contradiction by A14; :: thesis: verum

proof

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

then k0 = 0 by NAT_1:25;

hence contradiction by A127, A128; :: thesis: verum

end;then k0 = 0 by NAT_1:25;

hence contradiction by A127, A128; :: thesis: verum

then ( k0 <= k0 + 1 & n0 <= len p ) by FINSEQ_1:1, XREAL_1:29;

then k0 <= len p by A127, XXREAL_0:2;

then A131: k0 in Seg (len p) by A130, FINSEQ_1:1;

then A132: k0 in dom p by FINSEQ_1:def 3;

then A133: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by A122, A125, A127;

then A134: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by NECKLACE:def 3, ZFMISC_1:87;

p . n0 in the carrier of G by A127, A133, ZFMISC_1:87;

then A135: [(p . n0),(p . k0)] in the InternalRel of G by A127, A133, A134;

A136: for k being Nat st k > k0 & k in dom p holds

p . k in Y2

proof

k0 < n0
by A127, NAT_1:13;
assume
ex k being Nat st

( k > k0 & k in dom p & not p . k in Y2 ) ; :: thesis: contradiction

then consider k being Nat such that

A137: k > k0 and

A138: k in dom p and

A139: not p . k in Y2 ;

k > n0 hence contradiction by A125, A138, A139; :: thesis: verum

end;( k > k0 & k in dom p & not p . k in Y2 ) ; :: thesis: contradiction

then consider k being Nat such that

A137: k > k0 and

A138: k in dom p and

A139: not p . k in Y2 ;

k > n0 hence contradiction by A125, A138, A139; :: thesis: verum

then A140: not S

p . k0 in the carrier of G by A133, ZFMISC_1:87;

then ( p . k0 in the carrier of R or p . k0 in {x} ) by A19, XBOOLE_0:def 3;

then A141: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by A2, NECKLA_2:def 2;

thus ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G :: thesis: verum

proof
end;

per cases
( ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) or ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) or ( p . k0 in {x} & p . n0 in the carrier of G ) )
by A127, A133, A141, XBOOLE_0:def 3, ZFMISC_1:87;

end;

suppose
( p . k0 in the carrier of R2 & p . n0 in the carrier of G )
; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G

then reconsider m = p . k0 as Element of X2 by A22, A131, A140, A136, FINSEQ_1:def 3, XBOOLE_0:def 3;

reconsider l = p . n0 as Element of Y2 by A125;

[m,l] in the InternalRel of G by A122, A125, A127, A132;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A135; :: thesis: verum

end;reconsider l = p . n0 as Element of Y2 by A125;

[m,l] in the InternalRel of G by A122, A125, A127, A132;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A135; :: thesis: verum

suppose
( p . k0 in the carrier of R1 & p . n0 in the carrier of G )
; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G

then reconsider m = p . k0 as Element of R1 ;

reconsider l = p . n0 as Element of R2 by A22, A125, XBOOLE_0:def 3;

A142: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;

m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A143: m in the carrier of R by A2, NECKLA_2:def 2;

l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A144: l in the carrier of R by A2, NECKLA_2:def 2;

then [l,m] in [: the carrier of R, the carrier of R:] by A143, ZFMISC_1:87;

then [l,m] in the InternalRel of G |_2 the carrier of R by A135, XBOOLE_0:def 4;

then [l,m] in the InternalRel of R by YELLOW_0:def 14;

then [m,l] in the InternalRel of R by A144, A143, A142;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A1, A2, Th35; :: thesis: verum

end;reconsider l = p . n0 as Element of R2 by A22, A125, XBOOLE_0:def 3;

A142: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;

m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A143: m in the carrier of R by A2, NECKLA_2:def 2;

l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A144: l in the carrier of R by A2, NECKLA_2:def 2;

then [l,m] in [: the carrier of R, the carrier of R:] by A143, ZFMISC_1:87;

then [l,m] in the InternalRel of G |_2 the carrier of R by A135, XBOOLE_0:def 4;

then [l,m] in the InternalRel of R by YELLOW_0:def 14;

then [m,l] in the InternalRel of R by A144, A143, A142;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A1, A2, Th35; :: thesis: verum

suppose A145:
( p . k0 in {x} & p . n0 in the carrier of G )
; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G

ex y1 being Element of R2 st

( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A125;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A135, A145, TARSKI:def 1; :: thesis: verum

end;( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A125;

hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A135, A145, TARSKI:def 1; :: thesis: verum

A146: [u,v] in the InternalRel of G ;

set w = the Element of X1;

the Element of X1 in X1 by A10;

then A147: ex y being Element of R1 st

( y = the Element of X1 & [y,x] in the InternalRel of G ) ;

set Z = {u,v,x, the Element of X1};

{u,v,x, the Element of X1} c= the carrier of G

proof

then reconsider Z = {u,v,x, the Element of X1} as Subset of G ;
the Element of X1 in X1
by A10;

then ex y2 being Element of R1 st

( y2 = the Element of X1 & [y2,x] in the InternalRel of G ) ;

then the Element of X1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A148: the Element of X1 in the carrier of R by A2, NECKLA_2:def 2;

v in X2 by A18;

then ex y1 being Element of R2 st

( y1 = v & [y1,x] in the InternalRel of G ) ;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A149: v in the carrier of R by A2, NECKLA_2:def 2;

u in the carrier of R2 by A22, A115, XBOOLE_0:def 3;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A150: u in the carrier of R by A2, NECKLA_2:def 2;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X1} or q in the carrier of G )

assume q in {u,v,x, the Element of X1} ; :: thesis: q in the carrier of G

then A151: ( q = u or q = v or q = x or q = the Element of X1 ) by ENUMSET1:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

hence q in the carrier of G by A151, A150, A149, A148; :: thesis: verum

end;then ex y2 being Element of R1 st

( y2 = the Element of X1 & [y2,x] in the InternalRel of G ) ;

then the Element of X1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A148: the Element of X1 in the carrier of R by A2, NECKLA_2:def 2;

v in X2 by A18;

then ex y1 being Element of R2 st

( y1 = v & [y1,x] in the InternalRel of G ) ;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A149: v in the carrier of R by A2, NECKLA_2:def 2;

u in the carrier of R2 by A22, A115, XBOOLE_0:def 3;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then A150: u in the carrier of R by A2, NECKLA_2:def 2;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X1} or q in the carrier of G )

assume q in {u,v,x, the Element of X1} ; :: thesis: q in the carrier of G

then A151: ( q = u or q = v or q = x or q = the Element of X1 ) by ENUMSET1:def 2;

the carrier of R c= the carrier of G by A19, XBOOLE_1:7;

hence q in the carrier of G by A151, A150, A149, A148; :: thesis: verum

reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;

A152: the Element of X1 in X1 by A10;

reconsider w = the Element of X1 as Element of G by A147, ZFMISC_1:87;

A153: v in X2 by A18;

A154: [x,w] in the InternalRel of G

proof

A155:
u in Y2
by A115;
( ex y1 being Element of R1 st

( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by A152, NECKLACE:def 3;

hence [x,w] in the InternalRel of G ; :: thesis: verum

end;( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by A152, NECKLACE:def 3;

hence [x,w] in the InternalRel of G ; :: thesis: verum

reconsider u = u, v = v as Element of G by A146, ZFMISC_1:87;

A156: [v,x] in the InternalRel of G

proof

A157:
w <> u
ex y1 being Element of R2 st

( v = y1 & [y1,x] in the InternalRel of G ) by A153;

hence [v,x] in the InternalRel of G ; :: thesis: verum

end;( v = y1 & [y1,x] in the InternalRel of G ) by A153;

hence [v,x] in the InternalRel of G ; :: thesis: verum

proof

A159:
not [u,x] in the InternalRel of G
assume A158:
not w <> u
; :: thesis: contradiction

( ex y1 being Element of R1 st

( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( u = y2 & not [y2,x] in the InternalRel of G ) ) by A155, A152;

hence contradiction by A158; :: thesis: verum

end;( ex y1 being Element of R1 st

( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( u = y2 & not [y2,x] in the InternalRel of G ) ) by A155, A152;

hence contradiction by A158; :: thesis: verum

proof

A160:
not [v,w] in the InternalRel of G
ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

hence not [u,x] in the InternalRel of G ; :: thesis: verum

end;( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

hence not [u,x] in the InternalRel of G ; :: thesis: verum

proof

A164:
w <> x
A161:
ex y2 being Element of R1 st

( w = y2 & [y2,x] in the InternalRel of G ) by A152;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A162: ex y1 being Element of R2 st

( v = y1 & [y1,x] in the InternalRel of G ) by A153;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider v = v as Element of R by A2, NECKLA_2:def 2;

assume [v,w] in the InternalRel of G ; :: thesis: contradiction

then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [v,w] in the InternalRel of R by YELLOW_0:def 14;

then A163: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

end;( w = y2 & [y2,x] in the InternalRel of G ) by A152;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A162: ex y1 being Element of R2 st

( v = y1 & [y1,x] in the InternalRel of G ) by A153;

then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider v = v as Element of R by A2, NECKLA_2:def 2;

assume [v,w] in the InternalRel of G ; :: thesis: contradiction

then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [v,w] in the InternalRel of R by YELLOW_0:def 14;

then A163: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

per cases
( [v,w] in the InternalRel of R1 or [v,w] in the InternalRel of R2 )
by A163, XBOOLE_0:def 3;

end;

suppose
[v,w] in the InternalRel of R1
; :: thesis: contradiction

then
v in the carrier of R1
by ZFMISC_1:87;

then v in the carrier of R1 /\ the carrier of R2 by A162, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then v in the carrier of R1 /\ the carrier of R2 by A162, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

suppose
[v,w] in the InternalRel of R2
; :: thesis: contradiction

then
w in the carrier of R2
by ZFMISC_1:87;

then w in the carrier of R1 /\ the carrier of R2 by A161, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then w in the carrier of R1 /\ the carrier of R2 by A161, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

A166:
not [u,w] in the InternalRel of G
assume A165:
not w <> x
; :: thesis: contradiction

ex y1 being Element of R1 st

( w = y1 & [y1,x] in the InternalRel of G ) by A152;

then x in the carrier of R1 \/ the carrier of R2 by A165, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R1 st

( w = y1 & [y1,x] in the InternalRel of G ) by A152;

then x in the carrier of R1 \/ the carrier of R2 by A165, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

A170:
x <> u
A167:
ex y2 being Element of R1 st

( w = y2 & [y2,x] in the InternalRel of G ) by A152;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A168: ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider u = u as Element of R by A2, NECKLA_2:def 2;

assume [u,w] in the InternalRel of G ; :: thesis: contradiction

then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [u,w] in the InternalRel of R by YELLOW_0:def 14;

then A169: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

end;( w = y2 & [y2,x] in the InternalRel of G ) by A152;

then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider w = w as Element of R by A2, NECKLA_2:def 2;

A168: ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;

then reconsider u = u as Element of R by A2, NECKLA_2:def 2;

assume [u,w] in the InternalRel of G ; :: thesis: contradiction

then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;

then [u,w] in the InternalRel of R by YELLOW_0:def 14;

then A169: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by A2, NECKLA_2:def 2;

per cases
( [u,w] in the InternalRel of R1 or [u,w] in the InternalRel of R2 )
by A169, XBOOLE_0:def 3;

end;

suppose
[u,w] in the InternalRel of R1
; :: thesis: contradiction

then
u in the carrier of R1
by ZFMISC_1:87;

then u in the carrier of R1 /\ the carrier of R2 by A168, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then u in the carrier of R1 /\ the carrier of R2 by A168, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

suppose
[u,w] in the InternalRel of R2
; :: thesis: contradiction

then
w in the carrier of R2
by ZFMISC_1:87;

then w in the carrier of R1 /\ the carrier of R2 by A167, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;then w in the carrier of R1 /\ the carrier of R2 by A167, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

A172:
w <> v
assume A171:
not x <> u
; :: thesis: contradiction

ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

then x in the carrier of R1 \/ the carrier of R2 by A171, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) by A155;

then x in the carrier of R1 \/ the carrier of R2 by A171, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

A175:
v <> x
consider y1 being Element of R1 such that

A173: w = y1 and

[y1,x] in the InternalRel of G by A152;

assume A174: not w <> v ; :: thesis: contradiction

ex y2 being Element of R2 st

( v = y2 & [y2,x] in the InternalRel of G ) by A153;

then y1 in the carrier of R1 /\ the carrier of R2 by A174, A173, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

end;A173: w = y1 and

[y1,x] in the InternalRel of G by A152;

assume A174: not w <> v ; :: thesis: contradiction

ex y2 being Element of R2 st

( v = y2 & [y2,x] in the InternalRel of G ) by A153;

then y1 in the carrier of R1 /\ the carrier of R2 by A174, A173, XBOOLE_0:def 4;

hence contradiction by A1; :: thesis: verum

proof

u <> v
assume A176:
not v <> x
; :: thesis: contradiction

ex y1 being Element of R2 st

( v = y1 & [y1,x] in the InternalRel of G ) by A153;

then x in the carrier of R1 \/ the carrier of R2 by A176, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

end;ex y1 being Element of R2 st

( v = y1 & [y1,x] in the InternalRel of G ) by A153;

then x in the carrier of R1 \/ the carrier of R2 by A176, XBOOLE_0:def 3;

then x in the carrier of R by A2, NECKLA_2:def 2;

then x in the carrier of G \ {x} by YELLOW_0:def 15;

then not x in {x} by XBOOLE_0:def 5;

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

proof

then
u,v,x,w are_mutually_distinct
by A175, A170, A157, A172, A164, ZFMISC_1:def 6;
assume A177:
not u <> v
; :: thesis: contradiction

( ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( v = y2 & [y2,x] in the InternalRel of G ) ) by A155, A153;

hence contradiction by A177; :: thesis: verum

end;( ex y1 being Element of R2 st

( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st

( v = y2 & [y2,x] in the InternalRel of G ) ) by A155, A153;

hence contradiction by A177; :: thesis: verum

then A178: subrelstr Z embeds Necklace 4 by A146, A156, A154, A159, A166, A160, Th38;

G embeds Necklace 4

proof

hence
G embeds Necklace 4
; :: thesis: verum
assume
not G embeds Necklace 4
; :: thesis: contradiction

then G is N-free by NECKLA_2:def 1;

then H is N-free by Th23;

hence contradiction by A178, NECKLA_2:def 1; :: thesis: verum

end;then G is N-free by NECKLA_2:def 1;

then H is N-free by Th23;

hence contradiction by A178, NECKLA_2:def 1; :: thesis: verum