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:
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 ;
A11: rng () misses rng (1 .--> b)
proof
assume rng () meets rng (1 .--> b) ; :: thesis: contradiction
then consider x being object such that
A12: x in rng () and
A13: x in rng (1 .--> b) by XBOOLE_0:3;
rng () = {a} by FUNCOP_1:8;
then ( rng (1 .--> b) = {b} & x = a ) by ;
hence contradiction by A10, A13, TARSKI:def 1; :: thesis: verum
end;
set H = subrelstr Z;
set N4 = Necklace 4;
set IH = the InternalRel of ();
set cH = the carrier of ();
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 () is empty by ;
A15: (2,3) --> (c,d) = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;
A16: c <> d by ;
rng (2 .--> c) misses rng (3 .--> d)
proof
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 ;
hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum
end;
then A19: (2,3) --> (c,d) is one-to-one by ;
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
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 ;
( x = a or x = b ) by ;
hence contradiction by A2, A24, ZFMISC_1:def 6; :: thesis: verum
end;
dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = (dom ((0,1) --> (a,b))) \/ (dom ((2,3) --> (c,d))) by FUNCT_4:def 1
.= {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 () by ;
A26: dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d))
proof
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 ;
hence contradiction by A28, TARSKI:def 2; :: thesis: verum
end;
then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = (rng ((0,1) --> (a,b))) \/ (rng ((2,3) --> (c,d))) by NECKLACE:6;
then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = {a,b,c,d} by ;
then A29: rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of () by ;
then reconsider f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) as Function of (),() by ;
(0,1) --> (a,b) = () +* (1 .--> b) by FUNCT_4:def 4;
then A30: (0,1) --> (a,b) is one-to-one by ;
then A31: f is one-to-one by ;
A32: the InternalRel of () = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
proof
thus the InternalRel of () 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 ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of () or x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} )
A33: the carrier of () = Z by YELLOW_0:def 15;
assume A34: x in the InternalRel of () ; :: 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 () by YELLOW_0:def 14;
then A36: x in the InternalRel of G by XBOOLE_0:def 4;
x in [: the carrier of (), the carrier of ():] 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 ;
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
proof
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 ;
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 ; :: thesis: verum
end;
suppose x = [a,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [b,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
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 ; :: thesis: verum
end;
suppose x = [a,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ; :: thesis: verum
end;
suppose x = [a,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ; :: thesis: verum
end;
suppose x = [b,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [b,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ; :: thesis: verum
end;
end;
end;
end;
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
proof
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 ;
suppose x = [c,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A6, A36, A42; :: thesis: verum
end;
suppose x = [c,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [d,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A7, A36, A42; :: thesis: verum
end;
suppose x = [d,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A8, A36, A42; :: thesis: verum
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 ; :: thesis: verum
end;
suppose x = [c,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [d,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose A44: x = [d,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
not [d,d] 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 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
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 () )
assume A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} ; :: thesis: x in the InternalRel of ()
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 ;
suppose A46: x = [a,b] ; :: thesis: x in the InternalRel of ()
b in Z by ;
then A47: b in the carrier of () by YELLOW_0:def 15;
a in Z by ;
then a in the carrier of () by YELLOW_0:def 15;
then [a,b] in [: the carrier of (), the carrier of ():] by ;
then x in the InternalRel of G |_2 the carrier of () by ;
hence x in the InternalRel of () by YELLOW_0:def 14; :: thesis: verum
end;
suppose A51: x = [b,c] ; :: thesis: x in the InternalRel of ()
c in Z by ;
then A52: c in the carrier of () by YELLOW_0:def 15;
b in Z by ;
then b in the carrier of () by YELLOW_0:def 15;
then [b,c] in [: the carrier of (), the carrier of ():] by ;
then x in the InternalRel of G |_2 the carrier of () by ;
hence x in the InternalRel of () by YELLOW_0:def 14; :: thesis: verum
end;
suppose A56: x = [c,d] ; :: thesis: x in the InternalRel of ()
d in Z by ;
then A57: d in the carrier of () by YELLOW_0:def 15;
c in Z by ;
then c in the carrier of () by YELLOW_0:def 15;
then [c,d] in [: the carrier of (), the carrier of ():] by ;
then x in the InternalRel of G |_2 the carrier of () by ;
hence x in the InternalRel of () by YELLOW_0:def 14; :: thesis: verum
end;
end;
end;
for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of () )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of () )
thus ( [x,y] in the InternalRel of () implies [(f . x),(f . y)] in the InternalRel of () ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of () implies [x,y] in the InternalRel of () )
proof
assume A61: [x,y] in the InternalRel of () ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
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 ;
suppose A62: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
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
.= b by FUNCT_4:63 ;
A65: x = 0 by ;
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
.= a by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A66: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
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
.= a by FUNCT_4:63 ;
A69: x = 1 by ;
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
.= b by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A70: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
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
.= b by FUNCT_4:63 ;
A73: y = 2 by ;
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 ;
then f . y = ((2,3) --> (c,d)) . 2 by
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A75: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
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
.= b by FUNCT_4:63 ;
A78: x = 2 by ;
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 ;
then f . x = ((2,3) --> (c,d)) . 2 by
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A80: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
A81: ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by ;
A82: y = 3 by ;
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
.= d by FUNCT_4:63 ;
A84: x = 2 by ;
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
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A85: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of ()
A86: ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by ;
A87: y = 2 by ;
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
.= c by FUNCT_4:63 ;
A89: x = 3 by ;
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
.= d by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of () implies [x,y] in the InternalRel of () ) :: thesis: verum
proof
reconsider F = f " as Function of the carrier of (), the carrier of () by ;
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 ;
reconsider G = g " as Function of {a,b},{0,1} by ;
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 ;
reconsider Hh = h " as Function of {c,d},{2,3} by ;
A94: dom Hh = {c,d} by ;
A95: Hh = (c,d) --> (2,3) by ;
A96: F = G +* Hh by ;
A97: G = (a,b) --> (0,1) by ;
A98: dom G = {a,b} by ;
then G +* Hh = Hh +* G by ;
then A99: F = Hh +* G by ;
assume A100: [(f . x),(f . y)] in the InternalRel of () ; :: thesis: [x,y] in the InternalRel of ()
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 ;
suppose A101: [(f . x),(f . y)] = [a,b] ; :: thesis: [x,y] in the InternalRel of ()
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
.= 0 by ;
then A103: x = 0 by ;
A104: f . y = b by ;
then f . y in dom G by ;
then A105: F . (f . y) = G . b by
.= 1 by ;
F . (f . y) = y by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A106: [(f . x),(f . y)] = [b,a] ; :: thesis: [x,y] in the InternalRel of ()
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
.= 0 by ;
then A108: y = 0 by ;
A109: f . x = b by ;
then f . x in dom G by ;
then A110: F . (f . x) = G . b by
.= 1 by ;
F . (f . x) = x by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A111: [(f . x),(f . y)] = [b,c] ; :: thesis: [x,y] in the InternalRel of ()
then A112: f . x = b by XTUPLE_0:1;
then f . x in dom G by ;
then F . (f . x) = G . b by
.= 1 by ;
then A113: x = 1 by ;
A114: f . y = c by ;
then f . y in dom Hh by ;
then A115: F . (f . y) = Hh . c by
.= 2 by ;
F . (f . y) = y by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A116: [(f . x),(f . y)] = [c,b] ; :: thesis: [x,y] in the InternalRel of ()
then A117: f . y = b by XTUPLE_0:1;
then f . y in dom G by ;
then F . (f . y) = G . b by
.= 1 by ;
then A118: y = 1 by ;
A119: f . x = c by ;
then f . x in dom Hh by ;
then A120: F . (f . x) = Hh . c by
.= 2 by ;
F . (f . x) = x by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A121: [(f . x),(f . y)] = [c,d] ; :: thesis: [x,y] in the InternalRel of ()
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
.= 2 by ;
then A123: x = 2 by ;
A124: f . y = d by ;
then f . y in dom Hh by ;
then A125: F . (f . y) = Hh . d by
.= 3 by ;
F . (f . y) = y by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A126: [(f . x),(f . y)] = [d,c] ; :: thesis: [x,y] in the InternalRel of ()
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
.= 2 by ;
then A128: y = 2 by ;
A129: f . x = d by ;
then f . x in dom Hh by ;
then A130: F . (f . x) = Hh . d by
.= 3 by ;
F . (f . x) = x by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
end;
hence subrelstr Z embeds Necklace 4 by A31; :: thesis: verum