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 & G is path-connected & ComplRelStr G is path-connected )
; :: thesis: G embeds Necklace 4
set A = the carrier of G \ {x};
set X = {x};
reconsider X = {x} as Subset of G ;
set H = subrelstr X;
reconsider A = the carrier of G \ {x} as Subset of G ;
set R = subrelstr A;
not subrelstr A is empty
by A3, YELLOW_0:def 15;
then reconsider R = subrelstr A as non empty symmetric irreflexive RelStr ;
A4:
the carrier of G = the carrier of R \/ {x}
A7:
the carrier of (subrelstr X) misses the carrier of R
not subrelstr X is empty
by YELLOW_0:def 15;
then reconsider H = subrelstr X as non empty symmetric irreflexive RelStr ;
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 ;
A9:
X1 misses Y1
A13:
X2 misses Y2
A17:
R = subrelstr (([#] G) \ {x})
;
A18:
the carrier of R1 = X1 \/ Y1
A23:
the carrier of R2 = X2 \/ Y2
A28:
R = union_of R2,R1
by A2, Th8;
consider a being Element of R1 such that
A29:
[a,x] in the InternalRel of G
by A1, A2, A3, Th38;
A30:
a in X1
by A29;
consider b being Element of R2 such that
A31:
[b,x] in the InternalRel of G
by A1, A3, A17, A28, Th38;
A32:
b in X2
by A31;
A33:
not Y1 \/ Y2 is empty
proof
assume
Y1 \/ Y2 is
empty
;
:: thesis: contradiction
then A34:
(
Y1 is
empty &
Y2 is
empty )
;
A35:
for
a being
Element of
R holds
[a,x] in the
InternalRel of
G
not
ComplRelStr G is
path-connected
proof
assume A39:
ComplRelStr G is
path-connected
;
:: thesis: contradiction
A40:
a <> x
a is
Element of
(ComplRelStr G)
then
(
a is
Element of
(ComplRelStr G) &
x is
Element of
(ComplRelStr G) )
by NECKLACE:def 9;
then
the
InternalRel of
(ComplRelStr G) reduces x,
a
by A39, A40, Def2;
then consider p being
FinSequence such that A43:
(
len p > 0 &
p . 1
= x &
p . (len p) = a )
and A44:
for
i being
Element of
NAT st
i in dom p &
i + 1
in dom p holds
[(p . i),(p . (i + 1))] in the
InternalRel of
(ComplRelStr G)
by REWRITE1:12;
A45:
0 + 1
<= len p
by A43, NAT_1:13;
then
len p > 1
by A40, A43, XXREAL_0:1;
then
1
+ 1
<= len p
by NAT_1:13;
then
( 1
in dom p & 2
in dom p )
by A45, FINSEQ_3:27;
then A46:
[(p . 1),(p . (1 + 1))] in the
InternalRel of
(ComplRelStr G)
by A44;
then
p . 2
in the
carrier of
(ComplRelStr G)
by ZFMISC_1:106;
then A47:
p . 2
in the
carrier of
G
by NECKLACE:def 9;
A48:
p . 2
<> x
A50:
p . 2
in the
carrier of
R
A51:
(
p . 1
in the
carrier of
(ComplRelStr G) &
p . (1 + 1) in the
carrier of
(ComplRelStr G) )
by A46, ZFMISC_1:106;
the
InternalRel of
(ComplRelStr G) is_symmetric_in the
carrier of
(ComplRelStr G)
by NECKLACE:def 4;
then A52:
[(p . (1 + 1)),(p . 1)] in the
InternalRel of
(ComplRelStr G)
by A46, A51, RELAT_2:def 3;
[(p . 2),x] in the
InternalRel of
G
by A35, A50;
then
[(p . 2),x] in the
InternalRel of
(ComplRelStr G) /\ the
InternalRel of
G
by A43, A52, XBOOLE_0:def 4;
then
the
InternalRel of
(ComplRelStr G) meets the
InternalRel of
G
by XBOOLE_0:def 7;
hence
contradiction
by Th12;
:: thesis: verum
end;
hence
contradiction
by A3;
:: thesis: verum
end;
thus
G embeds Necklace 4
:: thesis: verumproof
per cases
( not Y1 is empty or not Y2 is empty )
by A33;
suppose A53:
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
proof
consider b being
Element of
Y1;
a in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A54:
a in the
carrier of
R
by A2, NECKLA_2:def 2;
A55:
the
carrier of
R c= the
carrier of
G
by A4, XBOOLE_1:7;
then reconsider a =
a as
Element of
G by A54;
b in Y1
by A53;
then consider y being
Element of
R1 such that A56:
(
y = b & not
[y,x] in the
InternalRel of
G )
;
b in the
carrier of
R1 \/ the
carrier of
R2
by A56, XBOOLE_0:def 3;
then
b in the
carrier of
R
by A2, NECKLA_2:def 2;
then reconsider b =
b as
Element of
G by A55;
a <> b
then
the
InternalRel of
G reduces a,
b
by A3, Def2;
then consider p being
FinSequence such that A57:
(
len p > 0 &
p . 1
= a &
p . (len p) = b )
and A58:
for
i being
Element of
NAT st
i in dom p &
i + 1
in dom p holds
[(p . i),(p . (i + 1))] in the
InternalRel of
G
by REWRITE1:12;
defpred S1[
Nat]
means (
p . $1
in Y1 & $1
in dom p & ( for
k being
Nat st
k > $1 &
k in dom p holds
p . k in Y1 ) );
A59:
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(A59);
then consider n0 being
Nat such that A62:
S1[
n0]
and A63:
for
n being
Nat st
S1[
n] holds
n >= n0
;
n0 <> 0
then consider k0 being
Nat such that A64:
n0 = k0 + 1
by NAT_1:6;
A65:
n0 <> 1
A66:
k0 in dom p
k0 < n0
by A64, NAT_1:13;
then A69:
not
S1[
k0]
by A63;
A70:
for
k being
Nat st
k > k0 &
k in dom p holds
p . k in Y1
A72:
[(p . k0),(p . (k0 + 1))] in the
InternalRel of
G
by A58, A62, A64, A66;
A73:
[(p . n0),(p . k0)] in the
InternalRel of
G
p . k0 in the
carrier of
G
by A72, ZFMISC_1:106;
then
(
p . k0 in the
carrier of
R or
p . k0 in {x} )
by A4, 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: 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 A64, A72, A75, XBOOLE_0:def 3, ZFMISC_1:106;
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 Gthen reconsider m =
p . k0 as
Element of
X1 by A18, A66, A69, A70, XBOOLE_0:def 3;
reconsider l =
p . n0 as
Element of
Y1 by A62;
A77:
[m,l] in the
InternalRel of
G
by A58, A62, A64, A66;
A78:
the
InternalRel of
G is_symmetric_in the
carrier of
G
by NECKLACE:def 4;
l in the
carrier of
R1
by A18, A62, 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 in the
carrier of
R1 \/ the
carrier of
R2
by A76, XBOOLE_0:def 3;
then A80:
m in the
carrier of
R
by A2, NECKLA_2:def 2;
the
carrier of
R c= the
carrier of
G
by A4, XBOOLE_1:7;
then
[l,m] in the
InternalRel of
G
by A77, A78, A79, A80, RELAT_2:def 3;
hence
ex
b being
Element of
Y1 ex
c being
Element of
X1 st
[b,c] in the
InternalRel of
G
;
:: thesis: verum end; 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 Gthen reconsider m =
p . k0 as
Element of
R2 ;
reconsider l =
p . n0 as
Element of
R1 by A18, A62, XBOOLE_0:def 3;
l in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A81:
l in the
carrier of
R
by A2, NECKLA_2:def 2;
m in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then
m in the
carrier of
R
by A2, NECKLA_2:def 2;
then
[l,m] in [:the carrier of R,the carrier of R:]
by A81, ZFMISC_1:106;
then
[l,m] in the
InternalRel of
G |_2 the
carrier of
R
by A73, 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, Th36;
:: thesis: verum end;
end;
end; then consider u being
Element of
Y1,
v being
Element of
X1 such that A84:
[u,v] in the
InternalRel of
G
;
consider w being
Element of
X2;
set Z =
{u,v,x,w};
{u,v,x,w} c= the
carrier of
G
proof
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x,w} or q in the carrier of G )
assume A85:
q in {u,v,x,w}
;
:: thesis: q in the carrier of G
A86:
(
q = u or
q = v or
q = x or
q = w )
by A85, ENUMSET1:def 2;
u in the
carrier of
R1
by A18, A53, XBOOLE_0:def 3;
then
u in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A87:
u in the
carrier of
R
by A2, NECKLA_2:def 2;
A88:
the
carrier of
R c= the
carrier of
G
by A4, XBOOLE_1:7;
v in X1
by A30;
then consider y1 being
Element of
R1 such that A89:
(
y1 = v &
[y1,x] in the
InternalRel of
G )
;
v in the
carrier of
R1 \/ the
carrier of
R2
by A89, XBOOLE_0:def 3;
then A90:
v in the
carrier of
R
by A2, NECKLA_2:def 2;
w in X2
by A32;
then consider y2 being
Element of
R2 such that A91:
(
y2 = w &
[y2,x] in the
InternalRel of
G )
;
w in the
carrier of
R1 \/ the
carrier of
R2
by A91, XBOOLE_0:def 3;
then
w in the
carrier of
R
by A2, NECKLA_2:def 2;
hence
q in the
carrier of
G
by A86, A87, A88, A90;
:: thesis: verum
end; then reconsider Z =
{u,v,x,w} as
Subset of
G ;
A92:
u in Y1
by A53;
A93:
v in X1
by A30;
A94:
w in X2
by A32;
reconsider u =
u,
v =
v as
Element of
G by A84, ZFMISC_1:106;
w in X2
by A32;
then consider y being
Element of
R2 such that A95:
(
y = w &
[y,x] in the
InternalRel of
G )
;
reconsider w =
w as
Element of
G by A95, ZFMISC_1:106;
(
u <> v &
v <> x &
x <> u &
w <> u &
w <> v &
w <> x )
then A116:
u,
v,
x,
w are_mutually_different
by ZFMISC_1:def 6;
A117:
[v,x] in the
InternalRel of
G
A119:
[x,w] in the
InternalRel of
G
A121:
not
[u,x] in the
InternalRel of
G
A123:
not
[u,w] in the
InternalRel of
G
proof
assume A124:
[u,w] in the
InternalRel of
G
;
:: thesis: contradiction
consider y1 being
Element of
R1 such that A125:
(
u = y1 & not
[y1,x] in the
InternalRel of
G )
by A92;
consider y2 being
Element of
R2 such that A126:
(
w = y2 &
[y2,x] in the
InternalRel of
G )
by A94;
u in the
carrier of
R1 \/ the
carrier of
R2
by A125, XBOOLE_0:def 3;
then reconsider u =
u as
Element of
R by A2, NECKLA_2:def 2;
w in the
carrier of
R1 \/ the
carrier of
R2
by A126, XBOOLE_0:def 3;
then reconsider w =
w as
Element of
R by A2, NECKLA_2:def 2;
[u,w] in the
InternalRel of
G |_2 the
carrier of
R
by A124, XBOOLE_0:def 4;
then
[u,w] in the
InternalRel of
R
by YELLOW_0:def 14;
then A127:
[u,w] in the
InternalRel of
R1 \/ the
InternalRel of
R2
by A2, NECKLA_2:def 2;
end;
not
[v,w] in the
InternalRel of
G
proof
assume A128:
[v,w] in the
InternalRel of
G
;
:: thesis: contradiction
consider y1 being
Element of
R1 such that A129:
(
v = y1 &
[y1,x] in the
InternalRel of
G )
by A93;
consider y2 being
Element of
R2 such that A130:
(
w = y2 &
[y2,x] in the
InternalRel of
G )
by A94;
v in the
carrier of
R1 \/ the
carrier of
R2
by A129, XBOOLE_0:def 3;
then reconsider v =
v as
Element of
R by A2, NECKLA_2:def 2;
w in the
carrier of
R1 \/ the
carrier of
R2
by A130, XBOOLE_0:def 3;
then reconsider w =
w as
Element of
R by A2, NECKLA_2:def 2;
[v,w] in the
InternalRel of
G |_2 the
carrier of
R
by A128, XBOOLE_0:def 4;
then
[v,w] in the
InternalRel of
R
by YELLOW_0:def 14;
then A131:
[v,w] in the
InternalRel of
R1 \/ the
InternalRel of
R2
by A2, NECKLA_2:def 2;
end; then A132:
subrelstr Z embeds Necklace 4
by A84, A116, A117, A119, A121, A123, Th39;
not
subrelstr Z is
empty
by YELLOW_0:def 15;
then reconsider H =
subrelstr Z as non
empty full SubRelStr of
G ;
G embeds Necklace 4
hence
G embeds Necklace 4
;
:: thesis: verum suppose A133:
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
proof
consider c being
Element of
Y2;
b in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A134:
b in the
carrier of
R
by A2, NECKLA_2:def 2;
A135:
the
carrier of
R c= the
carrier of
G
by A4, XBOOLE_1:7;
then reconsider b =
b as
Element of
G by A134;
c in Y2
by A133;
then consider y being
Element of
R2 such that A136:
(
y = c & not
[y,x] in the
InternalRel of
G )
;
c in the
carrier of
R1 \/ the
carrier of
R2
by A136, XBOOLE_0:def 3;
then
c in the
carrier of
R
by A2, NECKLA_2:def 2;
then reconsider c =
c as
Element of
G by A135;
b <> c
then
the
InternalRel of
G reduces b,
c
by A3, Def2;
then consider p being
FinSequence such that A137:
(
len p > 0 &
p . 1
= b &
p . (len p) = c )
and A138:
for
i being
Element of
NAT st
i in dom p &
i + 1
in dom p holds
[(p . i),(p . (i + 1))] in the
InternalRel of
G
by REWRITE1:12;
defpred S1[
Nat]
means (
p . $1
in Y2 & $1
in dom p & ( for
k being
Nat st
k > $1 &
k in dom p holds
p . k in Y2 ) );
A139:
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(A139);
then consider n0 being
Nat such that A142:
S1[
n0]
and A143:
for
n being
Nat st
S1[
n] holds
n >= n0
;
n0 <> 0
then consider k0 being
Nat such that A144:
n0 = k0 + 1
by NAT_1:6;
A145:
n0 <> 1
A146:
k0 in dom p
k0 < n0
by A144, NAT_1:13;
then A149:
not
S1[
k0]
by A143;
A150:
for
k being
Nat st
k > k0 &
k in dom p holds
p . k in Y2
A152:
[(p . k0),(p . (k0 + 1))] in the
InternalRel of
G
by A138, A142, A144, A146;
A153:
[(p . n0),(p . k0)] in the
InternalRel of
G
p . k0 in the
carrier of
G
by A152, ZFMISC_1:106;
then
(
p . k0 in the
carrier of
R or
p . k0 in {x} )
by A4, XBOOLE_0:def 3;
then A155:
(
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: 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 A144, A152, A155, XBOOLE_0:def 3, ZFMISC_1:106;
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 Gthen reconsider m =
p . k0 as
Element of
R1 ;
reconsider l =
p . n0 as
Element of
R2 by A23, A142, XBOOLE_0:def 3;
l in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A156:
l in the
carrier of
R
by A2, NECKLA_2:def 2;
m in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A157:
m in the
carrier of
R
by A2, NECKLA_2:def 2;
then
[l,m] in [:the carrier of R,the carrier of R:]
by A156, ZFMISC_1:106;
then
[l,m] in the
InternalRel of
G |_2 the
carrier of
R
by A153, XBOOLE_0:def 4;
then A158:
[l,m] in the
InternalRel of
R
by YELLOW_0:def 14;
the
InternalRel of
R is_symmetric_in the
carrier of
R
by NECKLACE:def 4;
then
[m,l] in the
InternalRel of
R
by A156, A157, A158, RELAT_2:def 3;
hence
ex
c being
Element of
Y2 ex
d being
Element of
X2 st
[c,d] in the
InternalRel of
G
by A1, A2, Th36;
:: thesis: verum end;
end;
end; then consider u being
Element of
Y2,
v being
Element of
X2 such that A161:
[u,v] in the
InternalRel of
G
;
consider w being
Element of
X1;
set Z =
{u,v,x,w};
{u,v,x,w} c= the
carrier of
G
proof
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x,w} or q in the carrier of G )
assume A162:
q in {u,v,x,w}
;
:: thesis: q in the carrier of G
A163:
(
q = u or
q = v or
q = x or
q = w )
by A162, ENUMSET1:def 2;
u in the
carrier of
R2
by A23, A133, XBOOLE_0:def 3;
then
u in the
carrier of
R1 \/ the
carrier of
R2
by XBOOLE_0:def 3;
then A164:
u in the
carrier of
R
by A2, NECKLA_2:def 2;
A165:
the
carrier of
R c= the
carrier of
G
by A4, XBOOLE_1:7;
v in X2
by A32;
then consider y1 being
Element of
R2 such that A166:
(
y1 = v &
[y1,x] in the
InternalRel of
G )
;
v in the
carrier of
R1 \/ the
carrier of
R2
by A166, XBOOLE_0:def 3;
then A167:
v in the
carrier of
R
by A2, NECKLA_2:def 2;
w in X1
by A30;
then consider y2 being
Element of
R1 such that A168:
(
y2 = w &
[y2,x] in the
InternalRel of
G )
;
w in the
carrier of
R1 \/ the
carrier of
R2
by A168, XBOOLE_0:def 3;
then
w in the
carrier of
R
by A2, NECKLA_2:def 2;
hence
q in the
carrier of
G
by A163, A164, A165, A167;
:: thesis: verum
end; then reconsider Z =
{u,v,x,w} as
Subset of
G ;
A169:
u in Y2
by A133;
A170:
v in X2
by A32;
A171:
w in X1
by A30;
reconsider u =
u,
v =
v as
Element of
G by A161, ZFMISC_1:106;
w in X1
by A30;
then consider y being
Element of
R1 such that A172:
(
y = w &
[y,x] in the
InternalRel of
G )
;
reconsider w =
w as
Element of
G by A172, ZFMISC_1:106;
(
u <> v &
v <> x &
x <> u &
w <> u &
w <> v &
w <> x )
then A193:
u,
v,
x,
w are_mutually_different
by ZFMISC_1:def 6;
A194:
[v,x] in the
InternalRel of
G
A196:
[x,w] in the
InternalRel of
G
A198:
not
[u,x] in the
InternalRel of
G
A200:
not
[u,w] in the
InternalRel of
G
proof
assume A201:
[u,w] in the
InternalRel of
G
;
:: thesis: contradiction
consider y1 being
Element of
R2 such that A202:
(
u = y1 & not
[y1,x] in the
InternalRel of
G )
by A169;
consider y2 being
Element of
R1 such that A203:
(
w = y2 &
[y2,x] in the
InternalRel of
G )
by A171;
u in the
carrier of
R1 \/ the
carrier of
R2
by A202, XBOOLE_0:def 3;
then reconsider u =
u as
Element of
R by A2, NECKLA_2:def 2;
w in the
carrier of
R1 \/ the
carrier of
R2
by A203, XBOOLE_0:def 3;
then reconsider w =
w as
Element of
R by A2, NECKLA_2:def 2;
[u,w] in the
InternalRel of
G |_2 the
carrier of
R
by A201, XBOOLE_0:def 4;
then
[u,w] in the
InternalRel of
R
by YELLOW_0:def 14;
then A204:
[u,w] in the
InternalRel of
R1 \/ the
InternalRel of
R2
by A2, NECKLA_2:def 2;
end;
not
[v,w] in the
InternalRel of
G
proof
assume A205:
[v,w] in the
InternalRel of
G
;
:: thesis: contradiction
consider y1 being
Element of
R2 such that A206:
(
v = y1 &
[y1,x] in the
InternalRel of
G )
by A170;
consider y2 being
Element of
R1 such that A207:
(
w = y2 &
[y2,x] in the
InternalRel of
G )
by A171;
v in the
carrier of
R1 \/ the
carrier of
R2
by A206, XBOOLE_0:def 3;
then reconsider v =
v as
Element of
R by A2, NECKLA_2:def 2;
w in the
carrier of
R1 \/ the
carrier of
R2
by A207, XBOOLE_0:def 3;
then reconsider w =
w as
Element of
R by A2, NECKLA_2:def 2;
[v,w] in the
InternalRel of
G |_2 the
carrier of
R
by A205, XBOOLE_0:def 4;
then
[v,w] in the
InternalRel of
R
by YELLOW_0:def 14;
then A208:
[v,w] in the
InternalRel of
R1 \/ the
InternalRel of
R2
by A2, NECKLA_2:def 2;
end; then A209:
subrelstr Z embeds Necklace 4
by A161, A193, A194, A196, A198, A200, Th39;
not
subrelstr Z is
empty
by YELLOW_0:def 15;
then reconsider H =
subrelstr Z as non
empty full SubRelStr of
G ;
G embeds Necklace 4
hence
G embeds Necklace 4
;
:: thesis: verum
end;