let G be non empty symmetric irreflexive 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) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds
G embeds Necklace 4
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) & 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 ; ( 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
; 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
A10:
a in X1
by A6;
A11:
the carrier of R1 = X1 \/ Y1
A14:
X2 misses Y2
A16:
the carrier of (subrelstr X) misses the carrier of R
reconsider H = subrelstr X as non empty symmetric irreflexive RelStr by YELLOW_0:def 15;
A18:
b in X2
by A7;
A19:
the carrier of G = the carrier of R \/ {x}
A22:
the carrier of R2 = X2 \/ Y2
A25:
not Y1 \/ Y2 is empty
proof
assume A26:
Y1 \/ Y2 is
empty
;
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
not
ComplRelStr G is
path-connected
proof
A31:
a <> x
a in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
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
;
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
p . 2
in the
carrier of
(ComplRelStr G)
by A42, ZFMISC_1:87;
then A45:
p . 2
in the
carrier of
G
by NECKLACE:def 8;
p . 2
in the
carrier of
R
then A46:
[(p . 2),x] in the
InternalRel of
G
by A29;
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;
verum
end;
hence
contradiction
by A5;
verum
end;
thus
G embeds Necklace 4
verumproof
per cases
( not Y1 is empty or not Y2 is empty )
by A25;
suppose A48:
not
Y1 is
empty
;
G embeds Necklace 4
ex
b being
Element of
Y1 ex
c being
Element of
X1 st
[b,c] in the
InternalRel of
G
proof
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
the
InternalRel of
G reduces a,
b
by A4;
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 S1[
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
then
S1[
len p]
by A48, A53, A55, CARD_1:27, FINSEQ_5:6;
then A58:
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(A58);
then consider n0 being
Nat such that A59:
S1[
n0]
and A60:
for
n being
Nat st
S1[
n] holds
n >= n0
;
n0 <> 0
then consider k0 being
Nat such that A61:
n0 = k0 + 1
by NAT_1:6;
A62:
n0 <> 1
A64:
k0 >= 1
n0 in Seg (len p)
by A59, FINSEQ_1:def 3;
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
assume
ex
k being
Nat st
(
k > k0 &
k in dom p & not
p . k in Y1 )
;
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;
verum
end;
k0 < n0
by A61, NAT_1:13;
then A74:
not
S1[
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
verumproof
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;
suppose A76:
(
p . k0 in the
carrier of
R1 &
p . n0 in the
carrier of
G )
;
ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of Gthen 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
;
verum end; suppose
(
p . k0 in the
carrier of
R2 &
p . n0 in the
carrier of
G )
;
ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of Gthen 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;
verum end;
end;
end; then consider u being
Element of
Y1,
v being
Element of
X1 such that 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
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 ;
TARSKI:def 3 ( 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}
;
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;
verum
end; then reconsider Z =
{u,v,x, the Element of X2} as
Subset 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
A91:
u in Y1
by A48;
reconsider u =
u,
v =
v as
Element of
G by A82, ZFMISC_1:87;
A92:
[v,x] in the
InternalRel of
G
A93:
w <> u
A95:
not
[u,x] in the
InternalRel of
G
A96:
not
[v,w] in the
InternalRel of
G
A100:
w <> x
A102:
not
[u,w] in the
InternalRel of
G
A106:
x <> u
A108:
w <> v
A111:
v <> x
u <> v
then
u,
v,
x,
w are_mutually_distinct
by A111, A106, A93, A108, A100, ZFMISC_1:def 6;
then A114:
subrelstr Z embeds Necklace 4
by A82, A92, A90, A95, A102, A96, Th38;
G embeds Necklace 4
hence
G embeds Necklace 4
;
verum suppose A115:
not
Y2 is
empty
;
G embeds Necklace 4
ex
c being
Element of
Y2 ex
d being
Element of
X2 st
[c,d] in the
InternalRel of
G
proof
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
the
InternalRel of
G reduces b,
c
by A4;
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 S1[
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
then
S1[
len p]
by A115, A119, A121, CARD_1:27, FINSEQ_5:6;
then A124:
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(A124);
then consider n0 being
Nat such that A125:
S1[
n0]
and A126:
for
n being
Nat st
S1[
n] holds
n >= n0
;
n0 <> 0
then consider k0 being
Nat such that A127:
n0 = k0 + 1
by NAT_1:6;
A128:
n0 <> 1
A130:
k0 >= 1
n0 in Seg (len p)
by A125, FINSEQ_1:def 3;
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
assume
ex
k being
Nat st
(
k > k0 &
k in dom p & not
p . k in Y2 )
;
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;
verum
end;
k0 < n0
by A127, NAT_1:13;
then A140:
not
S1[
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
verumproof
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;
suppose
(
p . k0 in the
carrier of
R2 &
p . n0 in the
carrier of
G )
;
ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of Gthen 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;
verum end; suppose
(
p . k0 in the
carrier of
R1 &
p . n0 in the
carrier of
G )
;
ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of Gthen 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;
verum end;
end;
end; then consider u being
Element of
Y2,
v being
Element of
X2 such that 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
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 ;
TARSKI:def 3 ( 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}
;
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;
verum
end; then reconsider Z =
{u,v,x, the Element of X1} as
Subset 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
A155:
u in Y2
by A115;
reconsider u =
u,
v =
v as
Element of
G by A146, ZFMISC_1:87;
A156:
[v,x] in the
InternalRel of
G
A157:
w <> u
A159:
not
[u,x] in the
InternalRel of
G
A160:
not
[v,w] in the
InternalRel of
G
A164:
w <> x
A166:
not
[u,w] in the
InternalRel of
G
A170:
x <> u
A172:
w <> v
A175:
v <> x
u <> v
then
u,
v,
x,
w are_mutually_distinct
by A175, A170, A157, A172, A164, ZFMISC_1:def 6;
then A178:
subrelstr Z embeds Necklace 4
by A146, A156, A154, A159, A166, A160, Th38;
G embeds Necklace 4
hence
G embeds Necklace 4
;
verum
end;