let R be non empty strict RelStr ; :: thesis: ( R in fin_RelStr_sp implies R is N-free )
set N4 = Necklace 4;
defpred S1[ Nat] means ex S being non empty strict RelStr st
( S in fin_RelStr_sp & card the carrier of S = \$1 & S embeds Necklace 4 );
assume A1: R in fin_RelStr_sp ; :: thesis: R is N-free
then ex S being strict RelStr st
( R = S & the carrier of S in FinSETS ) by Def4;
then reconsider C = the carrier of R as Element of FinSETS ;
set k = card C;
A2: for m being Nat st m <> 0 & S1[m] holds
ex n being Nat st
( n < m & S1[n] )
proof
let m be Nat; :: thesis: ( m <> 0 & S1[m] implies ex n being Nat st
( n < m & S1[n] ) )

assume that
m <> 0 and
A3: S1[m] ; :: thesis: ex n being Nat st
( n < m & S1[n] )

consider S being non empty strict RelStr such that
A4: S in fin_RelStr_sp and
A5: card the carrier of S = m and
A6: S embeds Necklace 4 by A3;
per cases ( S is 1 -element strict RelStr or ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( S = union_of (H1,H2) or S = sum_of (H1,H2) ) ) )
by ;
suppose A7: S is 1 -element strict RelStr ; :: thesis: ex n being Nat st
( n < m & S1[n] )

A8: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
A9: rng the InternalRel of S c= the carrier of S by RELAT_1:def 19;
consider f being Function of (),S such that
f is one-to-one and
A10: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of S ) by ;
A11: the carrier of () = {0,1,2,3} by ;
then A12: 0 in the carrier of () by ENUMSET1:def 2;
A13: 1 in the carrier of () by ;
( 0 = 0 + 1 or 1 = 0 + 1 ) ;
then [0,1] in the InternalRel of () by ;
then A14: [(f . 0),(f . 1)] in the InternalRel of S by ;
then A15: f . 1 in rng the InternalRel of S by XTUPLE_0:def 13;
f . 0 in dom the InternalRel of S by ;
then f . 0 = f . 1 by ;
then [0,0] in the InternalRel of () by ;
then ( [0,0] = [0,1] or [0,0] = [1,0] or [0,0] = [1,2] or [0,0] = [2,1] or [0,0] = [2,3] or [0,0] = [3,2] ) by ;
hence ex n being Nat st
( n < m & S1[n] ) by XTUPLE_0:1; :: thesis: verum
end;
suppose ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( S = union_of (H1,H2) or S = sum_of (H1,H2) ) ) ; :: thesis: ex n being Nat st
( n < m & S1[n] )

then consider H1, H2 being strict RelStr such that
A16: the carrier of H1 misses the carrier of H2 and
A17: H1 in fin_RelStr_sp and
A18: H2 in fin_RelStr_sp and
A19: ( S = union_of (H1,H2) or S = sum_of (H1,H2) ) ;
A20: now :: thesis: ( S = sum_of (H1,H2) implies ex n being Nat st
( n < m & S1[n] ) )
A21: not [1,3] in the InternalRel of ()
proof
assume A22: [1,3] in the InternalRel of () ; :: thesis: contradiction
per cases ( [1,3] = [0,1] or [1,3] = [1,2] or [1,3] = [2,3] or [1,3] = [3,2] or [1,3] = [2,1] or [1,3] = [1,0] ) by ;
end;
end;
A23: not [0,2] in the InternalRel of ()
proof
assume A24: [0,2] in the InternalRel of () ; :: thesis: contradiction
per cases ( [0,2] = [0,1] or [0,2] = [1,2] or [0,2] = [2,3] or [0,2] = [3,2] or [0,2] = [2,1] or [0,2] = [1,0] ) by ;
end;
end;
A25: the carrier of () = {0,1,2,3} by ;
then A26: 0 in the carrier of () by ENUMSET1:def 2;
A27: not [0,3] in the InternalRel of ()
proof
assume A28: [0,3] in the InternalRel of () ; :: thesis: contradiction
per cases ( [0,3] = [0,1] or [0,3] = [1,2] or [0,3] = [2,3] or [0,3] = [3,2] or [0,3] = [2,1] or [0,3] = [1,0] ) by ;
end;
end;
set A = the InternalRel of H1;
set B = the InternalRel of H2;
set C = [: the carrier of H1, the carrier of H2:];
set D = [: the carrier of H2, the carrier of H1:];
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
set cS = the carrier of S;
A29: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
assume A30: S = sum_of (H1,H2) ; :: thesis: ex n being Nat st
( n < m & S1[n] )

A31: [: the carrier of H1, the carrier of H2:] c= the InternalRel of S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of H1, the carrier of H2:] or x in the InternalRel of S )
assume x in [: the carrier of H1, the carrier of H2:] ; :: thesis: x in the InternalRel of S
then A32: x in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by XBOOLE_0:def 3;
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] c= (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_1:7;
then ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] c= the InternalRel of S by ;
hence x in the InternalRel of S by A32; :: thesis: verum
end;
A33: rng the InternalRel of S c= the carrier of S by RELAT_1:def 19;
A34: 3 in the carrier of () by ;
A35: [: the carrier of H2, the carrier of H1:] c= the InternalRel of S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of H2, the carrier of H1:] or x in the InternalRel of S )
( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] c= the InternalRel of H1 \/ (( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_1:7;
then ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] c= the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) by XBOOLE_1:4;
then ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] c= ( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_1:4;
then ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] c= (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_1:4;
then A36: ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] c= the InternalRel of S by ;
assume x in [: the carrier of H2, the carrier of H1:] ; :: thesis: x in the InternalRel of S
then x in ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_0:def 3;
hence x in the InternalRel of S by A36; :: thesis: verum
end;
A37: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
A38: 1 in the carrier of () by ;
consider f being Function of (),S such that
A39: f is one-to-one and
A40: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of S ) by ;
[1,0] in the InternalRel of () by ;
then A41: [(f . 1),(f . 0)] in the InternalRel of S by ;
A42: 2 in the carrier of () by ;
[3,2] in the InternalRel of () by ;
then A43: [(f . 3),(f . 2)] in the InternalRel of S by ;
[2,1] in the InternalRel of () by ;
then A44: [(f . 2),(f . 1)] in the InternalRel of S by ;
A45: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
[2,3] in the InternalRel of () by ;
then A46: [(f . 2),(f . 3)] in the InternalRel of S by ;
then f . 3 in rng the InternalRel of S by XTUPLE_0:def 13;
then f . 3 in the carrier of S by A33;
then A47: f . 3 in the carrier of H1 \/ the carrier of H2 by ;
[0,1] in the InternalRel of () by ;
then A48: [(f . 0),(f . 1)] in the InternalRel of S by ;
then f . 0 in dom the InternalRel of S by XTUPLE_0:def 12;
then f . 0 in the carrier of S by A29;
then A49: f . 0 in the carrier of H1 \/ the carrier of H2 by ;
f . 1 in rng the InternalRel of S by ;
then f . 1 in the carrier of S by A33;
then A50: f . 1 in the carrier of H1 \/ the carrier of H2 by ;
A51: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;
[1,2] in the InternalRel of () by ;
then A52: [(f . 1),(f . 2)] in the InternalRel of S by ;
then f . 2 in rng the InternalRel of S by XTUPLE_0:def 13;
then f . 2 in the carrier of S by A33;
then A53: f . 2 in the carrier of H1 \/ the carrier of H2 by ;
A54: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;
per cases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by ;
suppose A55: f . 0 in the carrier of H1 ; :: thesis: ex n being Nat st
( n < m & S1[n] )

set x1 = [(f . 0),(f . 1)];
set x2 = [(f . 1),(f . 2)];
set x3 = [(f . 2),(f . 3)];
set x4 = [(f . 1),(f . 0)];
set x5 = [(f . 2),(f . 1)];
set x6 = [(f . 3),(f . 2)];
A56: now :: thesis: not [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:]
assume [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ; :: thesis: contradiction
then f . 0 in the carrier of H2 by ZFMISC_1:87;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A57: now :: thesis: not f . 2 in the carrier of H2
assume f . 2 in the carrier of H2 ; :: thesis: contradiction
then [(f . 0),(f . 2)] in [: the carrier of H1, the carrier of H2:] by ;
hence contradiction by A40, A26, A42, A23, A31; :: thesis: verum
end;
A58: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H2
assume [(f . 1),(f . 0)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A45, A55, XBOOLE_0:3; :: thesis: verum
end;
A59: now :: thesis: not [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:]
assume [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:] ; :: thesis: contradiction
then f . 0 in the carrier of H2 by ZFMISC_1:87;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A60: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H2
assume [(f . 0),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A54, A55, XBOOLE_0:3; :: thesis: verum
end;
A61: now :: thesis: not f . 3 in the carrier of H2
assume f . 3 in the carrier of H2 ; :: thesis: contradiction
then [(f . 0),(f . 3)] in [: the carrier of H1, the carrier of H2:] by ;
hence contradiction by A40, A26, A34, A27, A31; :: thesis: verum
end;
then A62: f . 3 in the carrier of H1 by ;
A63: now :: thesis: not f . 1 in the carrier of H2
assume f . 1 in the carrier of H2 ; :: thesis: contradiction
then [(f . 1),(f . 3)] in [: the carrier of H2, the carrier of H1:] by ;
hence contradiction by A40, A38, A34, A21, A35; :: thesis: verum
end;
A64: dom f = the carrier of () by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H1 )
assume y in rng f ; :: thesis: y in the carrier of H1
then consider x being object such that
A65: x in dom f and
A66: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by ;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
end;
end;
then A67: f is Function of the carrier of (), the carrier of H1 by FUNCT_2:6;
H1 is finite by ;
then reconsider cH1 = the carrier of H1 as finite set ;
A68: H1 is non empty strict RelStr by ;
A69: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H2
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A45, A57; :: thesis: verum
end;
A70: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H2
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A54, A57; :: thesis: verum
end;
[(f . 1),(f . 0)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 1),(f . 0)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A71: [(f . 1),(f . 0)] in the InternalRel of H1 by ;
A72: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A54, A63; :: thesis: verum
end;
[(f . 1),(f . 2)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 1),(f . 2)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 1),(f . 2)] in [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A73: [(f . 1),(f . 2)] in the InternalRel of H1 by ;
[(f . 3),(f . 2)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 3),(f . 2)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 3),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 3),(f . 2)] in [: the carrier of H1, the carrier of H2:] or [(f . 3),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A74: [(f . 3),(f . 2)] in the InternalRel of H1 by ;
[(f . 2),(f . 3)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 2),(f . 3)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 3)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 2),(f . 3)] in [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 3)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A75: [(f . 2),(f . 3)] in the InternalRel of H1 by ;
A76: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H2
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A45, A63; :: thesis: verum
end;
H2 is finite by ;
then reconsider cH2 = the carrier of H2 as finite set ;
the carrier of S = cH1 \/ cH2 by ;
then reconsider cS = the carrier of S as finite set ;
A77: not H2 is empty by ;
A78: cH1 <> cS
proof
A79: cS = cH1 \/ cH2 by ;
assume A80: cH1 = cS ; :: thesis: contradiction
consider x being object such that
A81: x in cH2 by ;
cH1 /\ cH2 = {} by ;
then not x in cH1 by ;
hence contradiction by A80, A79, A81, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by ;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by ;
then A82: card cH1 < card cS by CARD_2:48;
[(f . 2),(f . 1)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 2),(f . 1)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 2),(f . 1)] in [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A83: [(f . 2),(f . 1)] in the InternalRel of H1 by ;
[(f . 0),(f . 1)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 0),(f . 1)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:] or [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A84: [(f . 0),(f . 1)] in the InternalRel of H1 by ;
for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H1 )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H1 )
thus ( [x,y] in the InternalRel of () implies [(f . x),(f . y)] in the InternalRel of H1 ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of () )
proof
assume A85: [x,y] in the InternalRel of () ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
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 A86: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A87: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A88: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A89: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A90: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A91: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of () ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of () ) by A40;
then ( [(f . x),(f . y)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] implies [x,y] in the InternalRel of () ) by ;
then ( [(f . x),(f . y)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) implies [x,y] in the InternalRel of () ) by XBOOLE_1:4;
then A92: ( [(f . x),(f . y)] in the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) implies [x,y] in the InternalRel of () ) by XBOOLE_1:4;
assume [(f . x),(f . y)] in the InternalRel of H1 ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
then H1 embeds Necklace 4 by ;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A17, A68, A82; :: thesis: verum
end;
suppose A93: f . 0 in the carrier of H2 ; :: thesis: ex n being Nat st
( n < m & S1[n] )

set x1 = [(f . 0),(f . 1)];
set x2 = [(f . 1),(f . 2)];
set x3 = [(f . 2),(f . 3)];
set x4 = [(f . 1),(f . 0)];
set x5 = [(f . 2),(f . 1)];
set x6 = [(f . 3),(f . 2)];
A94: now :: thesis: not [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:]
assume [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:] ; :: thesis: contradiction
then f . 0 in the carrier of H1 by ZFMISC_1:87;
hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum
end;
A95: now :: thesis: not [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:]
assume [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ; :: thesis: contradiction
then f . 0 in the carrier of H1 by ZFMISC_1:87;
hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum
end;
A96: now :: thesis: not f . 3 in the carrier of H1
assume f . 3 in the carrier of H1 ; :: thesis: contradiction
then [(f . 0),(f . 3)] in [: the carrier of H2, the carrier of H1:] by ;
hence contradiction by A40, A26, A34, A27, A35; :: thesis: verum
end;
then A97: f . 3 in the carrier of H2 by ;
A98: now :: thesis: not f . 1 in the carrier of H1
assume f . 1 in the carrier of H1 ; :: thesis: contradiction
then [(f . 1),(f . 3)] in [: the carrier of H1, the carrier of H2:] by ;
hence contradiction by A40, A38, A34, A21, A31; :: thesis: verum
end;
A99: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1
assume [(f . 1),(f . 0)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A51, A98; :: thesis: verum
end;
[(f . 1),(f . 0)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 1),(f . 0)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A100: [(f . 1),(f . 0)] in the InternalRel of H2 by ;
A101: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H1
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A98; :: thesis: verum
end;
A102: now :: thesis: not f . 2 in the carrier of H1
assume f . 2 in the carrier of H1 ; :: thesis: contradiction
then [(f . 0),(f . 2)] in [: the carrier of H2, the carrier of H1:] by ;
hence contradiction by A40, A26, A42, A23, A35; :: thesis: verum
end;
A103: dom f = the carrier of () by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H2 )
assume y in rng f ; :: thesis: y in the carrier of H2
then consider x being object such that
A104: x in dom f and
A105: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by ;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
end;
end;
then A106: f is Function of the carrier of (), the carrier of H2 by FUNCT_2:6;
H1 is finite by ;
then reconsider cH1 = the carrier of H1 as finite set ;
A107: H2 is non empty strict RelStr by ;
A108: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H1
assume [(f . 0),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A51, A93, XBOOLE_0:3; :: thesis: verum
end;
A109: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H1
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A102; :: thesis: verum
end;
A110: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H1
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A51, A102; :: thesis: verum
end;
[(f . 3),(f . 2)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 3),(f . 2)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 3),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 3),(f . 2)] in [: the carrier of H1, the carrier of H2:] or [(f . 3),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A111: [(f . 3),(f . 2)] in the InternalRel of H2 by ;
A112: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A102; :: thesis: verum
end;
[(f . 1),(f . 2)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 1),(f . 2)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 1),(f . 2)] in [: the carrier of H1, the carrier of H2:] or [(f . 1),(f . 2)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A113: [(f . 1),(f . 2)] in the InternalRel of H2 by ;
[(f . 2),(f . 3)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 2),(f . 3)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 3)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 2),(f . 3)] in [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 3)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A114: [(f . 2),(f . 3)] in the InternalRel of H2 by ;
[(f . 2),(f . 1)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 2),(f . 1)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 2),(f . 1)] in [: the carrier of H1, the carrier of H2:] or [(f . 2),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A115: [(f . 2),(f . 1)] in the InternalRel of H2 by ;
H2 is finite by ;
then reconsider cH2 = the carrier of H2 as finite set ;
the carrier of S = cH1 \/ cH2 by ;
then reconsider cS = the carrier of S as finite set ;
A116: not H1 is empty by ;
A117: cH2 <> cS
proof
A118: cS = cH1 \/ cH2 by ;
assume A119: cH2 = cS ; :: thesis: contradiction
consider x being object such that
A120: x in cH1 by ;
cH1 /\ cH2 = {} by ;
then not x in cH2 by ;
hence contradiction by A119, A118, A120, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by ;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by ;
then A121: card cH2 < card cS by CARD_2:48;
[(f . 0),(f . 1)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by ;
then ( [(f . 0),(f . 1)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] or [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then ( [(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 or [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:] or [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;
then A122: [(f . 0),(f . 1)] in the InternalRel of H2 by ;
for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H2 )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H2 )
thus ( [x,y] in the InternalRel of () implies [(f . x),(f . y)] in the InternalRel of H2 ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of () )
proof
assume A123: [x,y] in the InternalRel of () ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
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 A124: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A125: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A126: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A127: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A128: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A129: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of () ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of () ) by A40;
then ( [(f . x),(f . y)] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] implies [x,y] in the InternalRel of () ) by ;
then ( [(f . x),(f . y)] in ( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) implies [x,y] in the InternalRel of () ) by XBOOLE_1:4;
then A130: ( [(f . x),(f . y)] in the InternalRel of H2 \/ ( the InternalRel of H1 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) implies [x,y] in the InternalRel of () ) by XBOOLE_1:4;
assume [(f . x),(f . y)] in the InternalRel of H2 ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
then H2 embeds Necklace 4 by ;
hence ex n being Nat st
( n < m & S1[n] ) by ; :: thesis: verum
end;
end;
end;
now :: thesis: ( S = union_of (H1,H2) implies ex n being Nat st
( n < m & S1[n] ) )
A131: the carrier of () = {0,1,2,3} by ;
then A132: 0 in the carrier of () by ENUMSET1:def 2;
A133: 3 in the carrier of () by ;
A134: 1 in the carrier of () by ;
A135: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
consider f being Function of (),S such that
A136: f is one-to-one and
A137: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of S ) by ;
assume A138: S = union_of (H1,H2) ; :: thesis: ex n being Nat st
( n < m & S1[n] )

[0,1] in the InternalRel of () by ;
then A139: [(f . 0),(f . 1)] in the InternalRel of S by ;
then f . 0 in dom the InternalRel of S by XTUPLE_0:def 12;
then f . 0 in the carrier of S by A135;
then A140: f . 0 in the carrier of H1 \/ the carrier of H2 by ;
A141: 2 in the carrier of () by ;
[3,2] in the InternalRel of () by ;
then A142: [(f . 3),(f . 2)] in the InternalRel of S by ;
[2,3] in the InternalRel of () by ;
then A143: [(f . 2),(f . 3)] in the InternalRel of S by ;
[2,1] in the InternalRel of () by ;
then A144: [(f . 2),(f . 1)] in the InternalRel of S by ;
[1,2] in the InternalRel of () by ;
then A145: [(f . 1),(f . 2)] in the InternalRel of S by ;
[1,0] in the InternalRel of () by ;
then A146: [(f . 1),(f . 0)] in the InternalRel of S by ;
per cases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by ;
suppose A147: f . 0 in the carrier of H1 ; :: thesis: ex n being Nat st
( n < m & S1[n] )

set cS = the carrier of S;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A148: dom f = the carrier of () by FUNCT_2:def 1;
H2 is finite by ;
then reconsider cH2 = the carrier of H2 as finite set ;
H1 is finite by ;
then reconsider cH1 = the carrier of H1 as finite set ;
A149: the carrier of S = cH1 \/ cH2 by ;
A150: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;
A151: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H2
assume [(f . 0),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A147, A150, XBOOLE_0:3; :: thesis: verum
end;
A152: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
A153: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H2
assume [(f . 1),(f . 0)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A147, A152, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A154: [(f . 1),(f . 0)] in the InternalRel of H1 by ;
A155: H1 is non empty strict RelStr by ;
reconsider cS = the carrier of S as finite set by A149;
A156: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
[(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A157: [(f . 0),(f . 1)] in the InternalRel of H1 by ;
then A158: f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
A159: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H2
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A156, A152, A158, XBOOLE_0:3; :: thesis: verum
end;
A160: not H2 is empty by ;
A161: cH1 <> cS
proof
A162: cS = cH1 \/ cH2 by ;
assume A163: cH1 = cS ; :: thesis: contradiction
consider x being object such that
A164: x in cH2 by ;
cH1 /\ cH2 = {} by ;
then not x in cH1 by ;
hence contradiction by A163, A162, A164, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by ;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by ;
then A165: card cH1 < card cS by CARD_2:48;
A166: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
A167: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A156, A150, A158, XBOOLE_0:3; :: thesis: verum
end;
then A168: [(f . 1),(f . 2)] in the InternalRel of H1 by ;
then A169: f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H2
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A156, A150, A169, XBOOLE_0:3; :: thesis: verum
end;
then A170: [(f . 2),(f . 3)] in the InternalRel of H1 by ;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A171: [(f . 2),(f . 1)] in the InternalRel of H1 by ;
A172: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H2
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A156, A152, A169, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A173: [(f . 3),(f . 2)] in the InternalRel of H1 by ;
A174: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H1 )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H1 )
thus ( [x,y] in the InternalRel of () implies [(f . x),(f . y)] in the InternalRel of H1 ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of () )
proof
assume A175: [x,y] in the InternalRel of () ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
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 A176: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A177: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A178: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A179: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A180: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
suppose A181: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by ; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of () ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of () ) by A137;
then A182: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of () ) by ;
assume [(f . x),(f . y)] in the InternalRel of H1 ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
A183: f . 3 in rng the InternalRel of H1 by ;
rng f c= the carrier of H1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H1 )
assume y in rng f ; :: thesis: y in the carrier of H1
then consider x being object such that
A184: x in dom f and
A185: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by ;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by ; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (), the carrier of H1 by FUNCT_2:6;
then H1 embeds Necklace 4 by ;
hence ex n being Nat st
( n < m & S1[n] ) by ; :: thesis: verum
end;
suppose A186: f . 0 in the carrier of H2 ; :: thesis: ex n being Nat st
( n < m & S1[n] )

set cS = the carrier of S;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A187: dom f = the carrier of () by FUNCT_2:def 1;
H2 is finite by ;
then reconsider cH2 = the carrier of H2 as finite set ;
H1 is finite by ;
then reconsider cH1 = the carrier of H1 as finite set ;
A188: the carrier of S = cH1 \/ cH2 by ;
A189: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;
A190: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H1
assume [(f . 0),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A186, A189, XBOOLE_0:3; :: thesis: verum
end;
A191: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
A192: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1
assume [(f . 1),(f . 0)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A186, A191, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A193: [(f . 1),(f . 0)] in the InternalRel of H2 by ;
A194: H2 is non empty strict RelStr by ;
reconsider cS = the carrier of S as finite set by A188;
A195: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
[(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A196: [(f . 0),(f . 1)] in the InternalRel of H2 by ;
then A197: f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
A198: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H1
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A195, A191, A197, XBOOLE_0:3; :: thesis: verum
end;
A199: not H1 is empty by ;
A200: cH2 <> cS
proof
A201: cS = cH1 \/ cH2 by ;
assume A202: cH2 = cS ; :: thesis: contradiction
consider x being object such that
A203: x in cH1 by ;
cH1 /\ cH2 = {} by ;
then not x in cH2 by ;
hence contradiction by A202, A201, A203, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by ;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by ;
then A204: card cH2 < card cS by CARD_2:48;
A205: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
A206: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A195, A189, A197, XBOOLE_0:3; :: thesis: verum
end;
then A207: [(f . 1),(f . 2)] in the InternalRel of H2 by ;
then A208: f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H1
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A195, A189, A208, XBOOLE_0:3; :: thesis: verum
end;
then A209: [(f . 2),(f . 3)] in the InternalRel of H2 by ;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A210: [(f . 2),(f . 1)] in the InternalRel of H2 by ;
A211: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H1
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A195, A191, A208, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by ;
then A212: [(f . 3),(f . 2)] in the InternalRel of H2 by ;
A213: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H2 )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of H2 )
thus ( [x,y] in the InternalRel of () implies [(f . x),(f . y)] in the InternalRel of H2 ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of () )
proof
assume A214: [x,y] in the InternalRel of () ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
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 A215: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A216: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A217: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A218: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A219: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
suppose A220: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by ; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of () ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of () ) by A137;
then A221: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of () ) by ;
assume [(f . x),(f . y)] in the InternalRel of H2 ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
A222: f . 3 in rng the InternalRel of H2 by ;
rng f c= the carrier of H2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H2 )
assume y in rng f ; :: thesis: y in the carrier of H2
then consider x being object such that
A223: x in dom f and
A224: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by ;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by ; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (), the carrier of H2 by FUNCT_2:6;
then H2 embeds Necklace 4 by ;
hence ex n being Nat st
( n < m & S1[n] ) by ; :: thesis: verum
end;
end;
end;
hence ex n being Nat st
( n < m & S1[n] ) by ; :: thesis: verum
end;
end;
end;
assume R embeds Necklace 4 ; :: according to NECKLA_2:def 1 :: thesis: contradiction
then S1[ card C] by A1;
then A225: ex i being Nat st S1[i] ;
S1[ 0 ] from hence contradiction ; :: thesis: verum