let G be non empty symmetric irreflexive RelStr ; :: thesis: for a, b, c, d being Element of G

for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

let a, b, c, d be Element of G; :: thesis: for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

let Z be Subset of G; :: thesis: ( Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G implies subrelstr Z embeds Necklace 4 )

assume that

A1: Z = {a,b,c,d} and

A2: a,b,c,d are_mutually_distinct and

A3: [a,b] in the InternalRel of G and

A4: [b,c] in the InternalRel of G and

A5: [c,d] in the InternalRel of G and

A6: not [a,c] in the InternalRel of G and

A7: not [a,d] in the InternalRel of G and

A8: not [b,d] in the InternalRel of G ; :: thesis: subrelstr Z embeds Necklace 4

set g = (0,1) --> (a,b);

set h = (2,3) --> (c,d);

set f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d));

A9: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;

A10: a <> b by A2, ZFMISC_1:def 6;

A11: rng (0 .--> a) misses rng (1 .--> b)

set N4 = Necklace 4;

set IH = the InternalRel of (subrelstr Z);

set cH = the carrier of (subrelstr Z);

set IG = the InternalRel of G;

set X = {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]};

set Y = {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]};

A14: not the carrier of (subrelstr Z) is empty by A1, YELLOW_0:def 15;

A15: (2,3) --> (c,d) = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;

A16: c <> d by A2, ZFMISC_1:def 6;

rng (2 .--> c) misses rng (3 .--> d)

A20: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;

A21: rng ((0,1) --> (a,b)) misses rng ((2,3) --> (c,d))

.= {0,1} \/ (dom ((2,3) --> (c,d))) by FUNCT_4:62

.= {0,1} \/ {2,3} by FUNCT_4:62

.= {0,1,2,3} by ENUMSET1:5 ;

then A25: dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (Necklace 4) by NECKLACE:1, NECKLACE:20;

A26: dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d))

then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = {a,b,c,d} by A20, A9, ENUMSET1:5;

then A29: rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (subrelstr Z) by A1, YELLOW_0:def 15;

then reconsider f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) as Function of (Necklace 4),(subrelstr Z) by A25, FUNCT_2:def 1, RELSET_1:4;

(0,1) --> (a,b) = (0 .--> a) +* (1 .--> b) by FUNCT_4:def 4;

then A30: (0,1) --> (a,b) is one-to-one by A11, FUNCT_4:92;

then A31: f is one-to-one by A19, A21, FUNCT_4:92;

A32: the InternalRel of (subrelstr Z) = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (subrelstr Z) )

for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

let a, b, c, d be Element of G; :: thesis: for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

let Z be Subset of G; :: thesis: ( Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G implies subrelstr Z embeds Necklace 4 )

assume that

A1: Z = {a,b,c,d} and

A2: a,b,c,d are_mutually_distinct and

A3: [a,b] in the InternalRel of G and

A4: [b,c] in the InternalRel of G and

A5: [c,d] in the InternalRel of G and

A6: not [a,c] in the InternalRel of G and

A7: not [a,d] in the InternalRel of G and

A8: not [b,d] in the InternalRel of G ; :: thesis: subrelstr Z embeds Necklace 4

set g = (0,1) --> (a,b);

set h = (2,3) --> (c,d);

set f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d));

A9: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;

A10: a <> b by A2, ZFMISC_1:def 6;

A11: rng (0 .--> a) misses rng (1 .--> b)

proof

set H = subrelstr Z;
assume
rng (0 .--> a) meets rng (1 .--> b)
; :: thesis: contradiction

then consider x being object such that

A12: x in rng (0 .--> a) and

A13: x in rng (1 .--> b) by XBOOLE_0:3;

rng (0 .--> a) = {a} by FUNCOP_1:8;

then ( rng (1 .--> b) = {b} & x = a ) by A12, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A10, A13, TARSKI:def 1; :: thesis: verum

end;then consider x being object such that

A12: x in rng (0 .--> a) and

A13: x in rng (1 .--> b) by XBOOLE_0:3;

rng (0 .--> a) = {a} by FUNCOP_1:8;

then ( rng (1 .--> b) = {b} & x = a ) by A12, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A10, A13, TARSKI:def 1; :: thesis: verum

set N4 = Necklace 4;

set IH = the InternalRel of (subrelstr Z);

set cH = the carrier of (subrelstr Z);

set IG = the InternalRel of G;

set X = {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]};

set Y = {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]};

A14: not the carrier of (subrelstr Z) is empty by A1, YELLOW_0:def 15;

A15: (2,3) --> (c,d) = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;

A16: c <> d by A2, ZFMISC_1:def 6;

rng (2 .--> c) misses rng (3 .--> d)

proof

then A19:
(2,3) --> (c,d) is one-to-one
by A15, FUNCT_4:92;
assume
rng (2 .--> c) meets rng (3 .--> d)
; :: thesis: contradiction

then consider x being object such that

A17: x in rng (2 .--> c) and

A18: x in rng (3 .--> d) by XBOOLE_0:3;

rng (2 .--> c) = {c} by FUNCOP_1:8;

then ( rng (3 .--> d) = {d} & x = c ) by A17, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

end;then consider x being object such that

A17: x in rng (2 .--> c) and

A18: x in rng (3 .--> d) by XBOOLE_0:3;

rng (2 .--> c) = {c} by FUNCOP_1:8;

then ( rng (3 .--> d) = {d} & x = c ) by A17, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

A20: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;

A21: rng ((0,1) --> (a,b)) misses rng ((2,3) --> (c,d))

proof

dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) =
(dom ((0,1) --> (a,b))) \/ (dom ((2,3) --> (c,d)))
by FUNCT_4:def 1
assume
not rng ((0,1) --> (a,b)) misses rng ((2,3) --> (c,d))
; :: thesis: contradiction

then consider x being object such that

A22: x in rng ((0,1) --> (a,b)) and

A23: x in rng ((2,3) --> (c,d)) by XBOOLE_0:3;

A24: ( x = c or x = d ) by A9, A23, TARSKI:def 2;

( x = a or x = b ) by A20, A22, TARSKI:def 2;

hence contradiction by A2, A24, ZFMISC_1:def 6; :: thesis: verum

end;then consider x being object such that

A22: x in rng ((0,1) --> (a,b)) and

A23: x in rng ((2,3) --> (c,d)) by XBOOLE_0:3;

A24: ( x = c or x = d ) by A9, A23, TARSKI:def 2;

( x = a or x = b ) by A20, A22, TARSKI:def 2;

hence contradiction by A2, A24, ZFMISC_1:def 6; :: thesis: verum

.= {0,1} \/ (dom ((2,3) --> (c,d))) by FUNCT_4:62

.= {0,1} \/ {2,3} by FUNCT_4:62

.= {0,1,2,3} by ENUMSET1:5 ;

then A25: dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (Necklace 4) by NECKLACE:1, NECKLACE:20;

A26: dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d))

proof

then
rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = (rng ((0,1) --> (a,b))) \/ (rng ((2,3) --> (c,d)))
by NECKLACE:6;
assume
not dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d))
; :: thesis: contradiction

then consider x being object such that

A27: x in dom ((0,1) --> (a,b)) and

A28: x in dom ((2,3) --> (c,d)) by XBOOLE_0:3;

( x = 0 or x = 1 ) by A27, TARSKI:def 2;

hence contradiction by A28, TARSKI:def 2; :: thesis: verum

end;then consider x being object such that

A27: x in dom ((0,1) --> (a,b)) and

A28: x in dom ((2,3) --> (c,d)) by XBOOLE_0:3;

( x = 0 or x = 1 ) by A27, TARSKI:def 2;

hence contradiction by A28, TARSKI:def 2; :: thesis: verum

then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = {a,b,c,d} by A20, A9, ENUMSET1:5;

then A29: rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (subrelstr Z) by A1, YELLOW_0:def 15;

then reconsider f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) as Function of (Necklace 4),(subrelstr Z) by A25, FUNCT_2:def 1, RELSET_1:4;

(0,1) --> (a,b) = (0 .--> a) +* (1 .--> b) by FUNCT_4:def 4;

then A30: (0,1) --> (a,b) is one-to-one by A11, FUNCT_4:92;

then A31: f is one-to-one by A19, A21, FUNCT_4:92;

A32: the InternalRel of (subrelstr Z) = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

proof

for x, y being Element of (Necklace 4) holds
thus
the InternalRel of (subrelstr Z) c= {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
:: according to XBOOLE_0:def 10 :: thesis: {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} c= the InternalRel of (subrelstr Z)

assume A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} ; :: thesis: x in the InternalRel of (subrelstr Z)

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} or x in the InternalRel of (subrelstr Z) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (subrelstr Z) or x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} )

A33: the carrier of (subrelstr Z) = Z by YELLOW_0:def 15;

assume A34: x in the InternalRel of (subrelstr Z) ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

then A35: x in the InternalRel of G |_2 the carrier of (subrelstr Z) by YELLOW_0:def 14;

then A36: x in the InternalRel of G by XBOOLE_0:def 4;

x in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A34;

then A37: x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} \/ {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} by A1, A33, Th3;

end;A33: the carrier of (subrelstr Z) = Z by YELLOW_0:def 15;

assume A34: x in the InternalRel of (subrelstr Z) ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

then A35: x in the InternalRel of G |_2 the carrier of (subrelstr Z) by YELLOW_0:def 14;

then A36: x in the InternalRel of G by XBOOLE_0:def 4;

x in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A34;

then A37: x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} \/ {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} by A1, A33, Th3;

per cases
( x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} or x in {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} )
by A37, XBOOLE_0:def 3;

end;

suppose A38:
x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]}
; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

thus
x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
:: thesis: verum

end;proof
end;

per cases
( x = [a,a] or x = [a,b] or x = [b,a] or x = [b,b] or x = [a,c] or x = [a,d] or x = [b,c] or x = [b,d] )
by A38, ENUMSET1:def 6;

end;

suppose A39:
x = [a,a]
; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

not [a,a] in the InternalRel of G
by NECKLACE:def 5;

hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A39, XBOOLE_0:def 4; :: thesis: verum

end;hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A39, XBOOLE_0:def 4; :: thesis: verum

suppose A40:
x = [b,b]
; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

not [b,b] in the InternalRel of G
by NECKLACE:def 5;

hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A40, XBOOLE_0:def 4; :: thesis: verum

end;hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A40, XBOOLE_0:def 4; :: thesis: verum

suppose A41:
x in {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]}
; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

A42:
the InternalRel of G is_symmetric_in the carrier of G
by NECKLACE:def 3;

thus x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} :: thesis: verum

end;thus x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} :: thesis: verum

proof
end;

per cases
( x = [c,a] or x = [c,b] or x = [d,a] or x = [d,b] or x = [c,c] or x = [c,d] or x = [d,c] or x = [d,d] )
by A41, ENUMSET1:def 6;

end;

suppose A43:
x = [c,c]
; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}

not [c,c] in the InternalRel of G
by NECKLACE:def 5;

hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A43, XBOOLE_0:def 4; :: thesis: verum

end;hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A43, XBOOLE_0:def 4; :: thesis: verum

assume A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} ; :: thesis: x in the InternalRel of (subrelstr Z)

per cases
( x = [a,b] or x = [b,a] or x = [b,c] or x = [c,b] or x = [c,d] or x = [d,c] )
by A45, ENUMSET1:def 4;

end;

suppose A46:
x = [a,b]
; :: thesis: x in the InternalRel of (subrelstr Z)

b in Z
by A1, ENUMSET1:def 2;

then A47: b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

a in Z by A1, ENUMSET1:def 2;

then a in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [a,b] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A47, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A3, A46, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A47: b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

a in Z by A1, ENUMSET1:def 2;

then a in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [a,b] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A47, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A3, A46, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

suppose A48:
x = [b,a]
; :: thesis: x in the InternalRel of (subrelstr Z)

the InternalRel of G is_symmetric_in the carrier of G
by NECKLACE:def 3;

then A49: [b,a] in the InternalRel of G by A3;

a in Z by A1, ENUMSET1:def 2;

then A50: a in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [b,a] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A50, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A48, A49, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A49: [b,a] in the InternalRel of G by A3;

a in Z by A1, ENUMSET1:def 2;

then A50: a in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [b,a] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A50, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A48, A49, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

suppose A51:
x = [b,c]
; :: thesis: x in the InternalRel of (subrelstr Z)

c in Z
by A1, ENUMSET1:def 2;

then A52: c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [b,c] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A52, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A4, A51, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A52: c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [b,c] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A52, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A4, A51, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

suppose A53:
x = [c,b]
; :: thesis: x in the InternalRel of (subrelstr Z)

the InternalRel of G is_symmetric_in the carrier of G
by NECKLACE:def 3;

then A54: [c,b] in the InternalRel of G by A4;

c in Z by A1, ENUMSET1:def 2;

then A55: c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [c,b] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A55, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A53, A54, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A54: [c,b] in the InternalRel of G by A4;

c in Z by A1, ENUMSET1:def 2;

then A55: c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

b in Z by A1, ENUMSET1:def 2;

then b in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [c,b] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A55, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A53, A54, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

suppose A56:
x = [c,d]
; :: thesis: x in the InternalRel of (subrelstr Z)

d in Z
by A1, ENUMSET1:def 2;

then A57: d in the carrier of (subrelstr Z) by YELLOW_0:def 15;

c in Z by A1, ENUMSET1:def 2;

then c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [c,d] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A57, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A5, A56, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A57: d in the carrier of (subrelstr Z) by YELLOW_0:def 15;

c in Z by A1, ENUMSET1:def 2;

then c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [c,d] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A57, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A5, A56, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

suppose A58:
x = [d,c]
; :: thesis: x in the InternalRel of (subrelstr Z)

the InternalRel of G is_symmetric_in the carrier of G
by NECKLACE:def 3;

then A59: [d,c] in the InternalRel of G by A5;

d in Z by A1, ENUMSET1:def 2;

then A60: d in the carrier of (subrelstr Z) by YELLOW_0:def 15;

c in Z by A1, ENUMSET1:def 2;

then c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [d,c] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A60, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A58, A59, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

end;then A59: [d,c] in the InternalRel of G by A5;

d in Z by A1, ENUMSET1:def 2;

then A60: d in the carrier of (subrelstr Z) by YELLOW_0:def 15;

c in Z by A1, ENUMSET1:def 2;

then c in the carrier of (subrelstr Z) by YELLOW_0:def 15;

then [d,c] in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A60, ZFMISC_1:87;

then x in the InternalRel of G |_2 the carrier of (subrelstr Z) by A58, A59, XBOOLE_0:def 4;

hence x in the InternalRel of (subrelstr Z) by YELLOW_0:def 14; :: thesis: verum

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (subrelstr Z) )

proof

hence
subrelstr Z embeds Necklace 4
by A31; :: thesis: verum
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (subrelstr Z) )

thus ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of (subrelstr Z) implies [x,y] in the InternalRel of (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of (subrelstr Z) implies [x,y] in the InternalRel of (Necklace 4) )

proof

thus
( [(f . x),(f . y)] in the InternalRel of (subrelstr Z) implies [x,y] in the InternalRel of (Necklace 4) )
:: thesis: verum
assume A61:
[x,y] in the InternalRel of (Necklace 4)
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

end;per cases
( [x,y] = [0,1] or [x,y] = [1,0] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] )
by A61, ENUMSET1:def 4, NECKLA_2:2;

end;

suppose A62:
[x,y] = [0,1]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

then A63:
y = 1
by XTUPLE_0:1;

then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A64: f . y = ((0,1) --> (a,b)) . 1 by A26, A63, FUNCT_4:16

.= b by FUNCT_4:63 ;

A65: x = 0 by A62, XTUPLE_0:1;

then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then f . x = ((0,1) --> (a,b)) . 0 by A26, A65, FUNCT_4:16

.= a by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A64, ENUMSET1:def 4; :: thesis: verum

end;then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A64: f . y = ((0,1) --> (a,b)) . 1 by A26, A63, FUNCT_4:16

.= b by FUNCT_4:63 ;

A65: x = 0 by A62, XTUPLE_0:1;

then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then f . x = ((0,1) --> (a,b)) . 0 by A26, A65, FUNCT_4:16

.= a by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A64, ENUMSET1:def 4; :: thesis: verum

suppose A66:
[x,y] = [1,0]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

then A67:
y = 0
by XTUPLE_0:1;

then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A68: f . y = ((0,1) --> (a,b)) . 0 by A26, A67, FUNCT_4:16

.= a by FUNCT_4:63 ;

A69: x = 1 by A66, XTUPLE_0:1;

then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then f . x = ((0,1) --> (a,b)) . 1 by A26, A69, FUNCT_4:16

.= b by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A68, ENUMSET1:def 4; :: thesis: verum

end;then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A68: f . y = ((0,1) --> (a,b)) . 0 by A26, A67, FUNCT_4:16

.= a by FUNCT_4:63 ;

A69: x = 1 by A66, XTUPLE_0:1;

then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then f . x = ((0,1) --> (a,b)) . 1 by A26, A69, FUNCT_4:16

.= b by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A68, ENUMSET1:def 4; :: thesis: verum

suppose A70:
[x,y] = [1,2]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

then A71:
x = 1
by XTUPLE_0:1;

then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A72: f . x = ((0,1) --> (a,b)) . 1 by A26, A71, FUNCT_4:16

.= b by FUNCT_4:63 ;

A73: y = 2 by A70, XTUPLE_0:1;

then y in {2,3} by TARSKI:def 2;

then A74: y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;

then f . y = ((2,3) --> (c,d)) . 2 by A26, A73, A74, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A72, ENUMSET1:def 4; :: thesis: verum

end;then x in {0,1} by TARSKI:def 2;

then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A72: f . x = ((0,1) --> (a,b)) . 1 by A26, A71, FUNCT_4:16

.= b by FUNCT_4:63 ;

A73: y = 2 by A70, XTUPLE_0:1;

then y in {2,3} by TARSKI:def 2;

then A74: y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;

then f . y = ((2,3) --> (c,d)) . 2 by A26, A73, A74, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A72, ENUMSET1:def 4; :: thesis: verum

suppose A75:
[x,y] = [2,1]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

then A76:
y = 1
by XTUPLE_0:1;

then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A77: f . y = ((0,1) --> (a,b)) . 1 by A26, A76, FUNCT_4:16

.= b by FUNCT_4:63 ;

A78: x = 2 by A75, XTUPLE_0:1;

then x in {2,3} by TARSKI:def 2;

then A79: x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;

then f . x = ((2,3) --> (c,d)) . 2 by A26, A78, A79, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A77, ENUMSET1:def 4; :: thesis: verum

end;then y in {0,1} by TARSKI:def 2;

then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;

then A77: f . y = ((0,1) --> (a,b)) . 1 by A26, A76, FUNCT_4:16

.= b by FUNCT_4:63 ;

A78: x = 2 by A75, XTUPLE_0:1;

then x in {2,3} by TARSKI:def 2;

then A79: x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;

then f . x = ((2,3) --> (c,d)) . 2 by A26, A78, A79, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A77, ENUMSET1:def 4; :: thesis: verum

suppose A80:
[x,y] = [2,3]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

A81:
((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b))
by A26, FUNCT_4:35;

A82: y = 3 by A80, XTUPLE_0:1;

then y in {2,3} by TARSKI:def 2;

then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then A83: f . y = ((2,3) --> (c,d)) . 3 by A26, A82, A81, FUNCT_4:16

.= d by FUNCT_4:63 ;

A84: x = 2 by A80, XTUPLE_0:1;

then x in {2,3} by TARSKI:def 2;

then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then f . x = ((2,3) --> (c,d)) . 2 by A26, A84, A81, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A83, ENUMSET1:def 4; :: thesis: verum

end;A82: y = 3 by A80, XTUPLE_0:1;

then y in {2,3} by TARSKI:def 2;

then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then A83: f . y = ((2,3) --> (c,d)) . 3 by A26, A82, A81, FUNCT_4:16

.= d by FUNCT_4:63 ;

A84: x = 2 by A80, XTUPLE_0:1;

then x in {2,3} by TARSKI:def 2;

then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then f . x = ((2,3) --> (c,d)) . 2 by A26, A84, A81, FUNCT_4:16

.= c by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A83, ENUMSET1:def 4; :: thesis: verum

suppose A85:
[x,y] = [3,2]
; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)

A86:
((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b))
by A26, FUNCT_4:35;

A87: y = 2 by A85, XTUPLE_0:1;

then y in {3,2} by TARSKI:def 2;

then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then A88: f . y = ((2,3) --> (c,d)) . 2 by A26, A87, A86, FUNCT_4:16

.= c by FUNCT_4:63 ;

A89: x = 3 by A85, XTUPLE_0:1;

then x in {3,2} by TARSKI:def 2;

then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then f . x = ((2,3) --> (c,d)) . 3 by A26, A89, A86, FUNCT_4:16

.= d by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A88, ENUMSET1:def 4; :: thesis: verum

end;A87: y = 2 by A85, XTUPLE_0:1;

then y in {3,2} by TARSKI:def 2;

then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then A88: f . y = ((2,3) --> (c,d)) . 2 by A26, A87, A86, FUNCT_4:16

.= c by FUNCT_4:63 ;

A89: x = 3 by A85, XTUPLE_0:1;

then x in {3,2} by TARSKI:def 2;

then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;

then f . x = ((2,3) --> (c,d)) . 3 by A26, A89, A86, FUNCT_4:16

.= d by FUNCT_4:63 ;

hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A88, ENUMSET1:def 4; :: thesis: verum

proof

reconsider F = f " as Function of the carrier of (subrelstr Z), the carrier of (Necklace 4) by A29, A31, FUNCT_2:25;

A90: dom ((0,1) --> (a,b)) = {0,1} by FUNCT_4:62;

A91: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;

then reconsider g = (0,1) --> (a,b) as Function of {0,1},{a,b} by A90, RELSET_1:4;

reconsider G = g " as Function of {a,b},{0,1} by A20, A30, FUNCT_2:25;

A92: dom ((2,3) --> (c,d)) = {2,3} by FUNCT_4:62;

A93: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;

then reconsider h = (2,3) --> (c,d) as Function of {2,3},{c,d} by A92, RELSET_1:4;

reconsider Hh = h " as Function of {c,d},{2,3} by A9, A19, FUNCT_2:25;

A94: dom Hh = {c,d} by A19, A93, FUNCT_1:33;

A95: Hh = (c,d) --> (2,3) by A16, NECKLACE:10;

A96: F = G +* Hh by A26, A30, A19, A21, NECKLACE:7;

A97: G = (a,b) --> (0,1) by A10, NECKLACE:10;

A98: dom G = {a,b} by A30, A91, FUNCT_1:33;

then G +* Hh = Hh +* G by A20, A9, A21, A94, FUNCT_4:35;

then A99: F = Hh +* G by A26, A30, A19, A21, NECKLACE:7;

assume A100: [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)

end;A90: dom ((0,1) --> (a,b)) = {0,1} by FUNCT_4:62;

A91: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;

then reconsider g = (0,1) --> (a,b) as Function of {0,1},{a,b} by A90, RELSET_1:4;

reconsider G = g " as Function of {a,b},{0,1} by A20, A30, FUNCT_2:25;

A92: dom ((2,3) --> (c,d)) = {2,3} by FUNCT_4:62;

A93: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;

then reconsider h = (2,3) --> (c,d) as Function of {2,3},{c,d} by A92, RELSET_1:4;

reconsider Hh = h " as Function of {c,d},{2,3} by A9, A19, FUNCT_2:25;

A94: dom Hh = {c,d} by A19, A93, FUNCT_1:33;

A95: Hh = (c,d) --> (2,3) by A16, NECKLACE:10;

A96: F = G +* Hh by A26, A30, A19, A21, NECKLACE:7;

A97: G = (a,b) --> (0,1) by A10, NECKLACE:10;

A98: dom G = {a,b} by A30, A91, FUNCT_1:33;

then G +* Hh = Hh +* G by A20, A9, A21, A94, FUNCT_4:35;

then A99: F = Hh +* G by A26, A30, A19, A21, NECKLACE:7;

assume A100: [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)

per cases
( [(f . x),(f . y)] = [a,b] or [(f . x),(f . y)] = [b,a] or [(f . x),(f . y)] = [b,c] or [(f . x),(f . y)] = [c,b] or [(f . x),(f . y)] = [c,d] or [(f . x),(f . y)] = [d,c] )
by A32, A100, ENUMSET1:def 4;

end;

suppose A101:
[(f . x),(f . y)] = [a,b]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A102:
f . x = a
by XTUPLE_0:1;

then f . x in {a,b} by TARSKI:def 2;

then F . (f . x) = G . a by A20, A9, A21, A98, A94, A96, A102, FUNCT_4:16

.= 0 by A10, A97, FUNCT_4:63 ;

then A103: x = 0 by A14, A31, FUNCT_2:26;

A104: f . y = b by A101, XTUPLE_0:1;

then f . y in dom G by A98, TARSKI:def 2;

then A105: F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A104, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A103, A105, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . x in {a,b} by TARSKI:def 2;

then F . (f . x) = G . a by A20, A9, A21, A98, A94, A96, A102, FUNCT_4:16

.= 0 by A10, A97, FUNCT_4:63 ;

then A103: x = 0 by A14, A31, FUNCT_2:26;

A104: f . y = b by A101, XTUPLE_0:1;

then f . y in dom G by A98, TARSKI:def 2;

then A105: F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A104, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A103, A105, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

suppose A106:
[(f . x),(f . y)] = [b,a]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A107:
f . y = a
by XTUPLE_0:1;

then f . y in {a,b} by TARSKI:def 2;

then F . (f . y) = G . a by A20, A9, A21, A98, A94, A96, A107, FUNCT_4:16

.= 0 by A10, A97, FUNCT_4:63 ;

then A108: y = 0 by A14, A31, FUNCT_2:26;

A109: f . x = b by A106, XTUPLE_0:1;

then f . x in dom G by A98, TARSKI:def 2;

then A110: F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A109, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A108, A110, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . y in {a,b} by TARSKI:def 2;

then F . (f . y) = G . a by A20, A9, A21, A98, A94, A96, A107, FUNCT_4:16

.= 0 by A10, A97, FUNCT_4:63 ;

then A108: y = 0 by A14, A31, FUNCT_2:26;

A109: f . x = b by A106, XTUPLE_0:1;

then f . x in dom G by A98, TARSKI:def 2;

then A110: F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A109, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A108, A110, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

suppose A111:
[(f . x),(f . y)] = [b,c]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A112:
f . x = b
by XTUPLE_0:1;

then f . x in dom G by A98, TARSKI:def 2;

then F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A112, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

then A113: x = 1 by A14, A31, FUNCT_2:26;

A114: f . y = c by A111, XTUPLE_0:1;

then f . y in dom Hh by A94, TARSKI:def 2;

then A115: F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A114, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A113, A115, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . x in dom G by A98, TARSKI:def 2;

then F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A112, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

then A113: x = 1 by A14, A31, FUNCT_2:26;

A114: f . y = c by A111, XTUPLE_0:1;

then f . y in dom Hh by A94, TARSKI:def 2;

then A115: F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A114, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A113, A115, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

suppose A116:
[(f . x),(f . y)] = [c,b]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A117:
f . y = b
by XTUPLE_0:1;

then f . y in dom G by A98, TARSKI:def 2;

then F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A117, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

then A118: y = 1 by A14, A31, FUNCT_2:26;

A119: f . x = c by A116, XTUPLE_0:1;

then f . x in dom Hh by A94, TARSKI:def 2;

then A120: F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A119, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A118, A120, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . y in dom G by A98, TARSKI:def 2;

then F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A117, FUNCT_4:16

.= 1 by A97, FUNCT_4:63 ;

then A118: y = 1 by A14, A31, FUNCT_2:26;

A119: f . x = c by A116, XTUPLE_0:1;

then f . x in dom Hh by A94, TARSKI:def 2;

then A120: F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A119, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A118, A120, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

suppose A121:
[(f . x),(f . y)] = [c,d]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A122:
f . x = c
by XTUPLE_0:1;

then f . x in {c,d} by TARSKI:def 2;

then F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A122, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

then A123: x = 2 by A14, A31, FUNCT_2:26;

A124: f . y = d by A121, XTUPLE_0:1;

then f . y in dom Hh by A94, TARSKI:def 2;

then A125: F . (f . y) = Hh . d by A20, A9, A21, A98, A94, A99, A124, FUNCT_4:16

.= 3 by A95, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A123, A125, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . x in {c,d} by TARSKI:def 2;

then F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A122, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

then A123: x = 2 by A14, A31, FUNCT_2:26;

A124: f . y = d by A121, XTUPLE_0:1;

then f . y in dom Hh by A94, TARSKI:def 2;

then A125: F . (f . y) = Hh . d by A20, A9, A21, A98, A94, A99, A124, FUNCT_4:16

.= 3 by A95, FUNCT_4:63 ;

F . (f . y) = y by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A123, A125, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

suppose A126:
[(f . x),(f . y)] = [d,c]
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then A127:
f . y = c
by XTUPLE_0:1;

then f . y in {c,d} by TARSKI:def 2;

then F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A127, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

then A128: y = 2 by A14, A31, FUNCT_2:26;

A129: f . x = d by A126, XTUPLE_0:1;

then f . x in dom Hh by A94, TARSKI:def 2;

then A130: F . (f . x) = Hh . d by A20, A9, A21, A98, A94, A99, A129, FUNCT_4:16

.= 3 by A95, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A128, A130, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum

end;then f . y in {c,d} by TARSKI:def 2;

then F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A127, FUNCT_4:16

.= 2 by A16, A95, FUNCT_4:63 ;

then A128: y = 2 by A14, A31, FUNCT_2:26;

A129: f . x = d by A126, XTUPLE_0:1;

then f . x in dom Hh by A94, TARSKI:def 2;

then A130: F . (f . x) = Hh . d by A20, A9, A21, A98, A94, A99, A129, FUNCT_4:16

.= 3 by A95, FUNCT_4:63 ;

F . (f . x) = x by A14, A31, FUNCT_2:26;

hence [x,y] in the InternalRel of (Necklace 4) by A128, A130, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum