let R be non empty strict RelStr ; :: thesis: ( R in fin_RelStr_sp implies R is N-free )

set N4 = Necklace 4;

defpred S_{1}[ 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 & S_{1}[m] holds

ex n being Nat st

( n < m & S_{1}[n] )

then S_{1}[ card C]
by A1;

then A225: ex i being Nat st S_{1}[i]
;

S_{1}[ 0 ]
from NAT_1:sch 7(A225, A2);

hence contradiction ; :: thesis: verum

set N4 = Necklace 4;

defpred S

( 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 & S

ex n being Nat st

( n < m & S

proof

assume
R embeds Necklace 4
; :: according to NECKLA_2:def 1 :: thesis: contradiction
let m be Nat; :: thesis: ( m <> 0 & S_{1}[m] implies ex n being Nat st

( n < m & S_{1}[n] ) )

assume that

m <> 0 and

A3: S_{1}[m]
; :: thesis: ex n being Nat st

( n < m & S_{1}[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;

end;( n < m & S

assume that

m <> 0 and

A3: S

( n < m & S

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 A4, Th6;

end;

( 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 A4, Th6;

suppose A7:
S is 1 -element strict RelStr
; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

( n < m & S

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 (Necklace 4),S such that

f is one-to-one and

A10: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

A11: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;

then A12: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A13: 1 in the carrier of (Necklace 4) by A11, ENUMSET1:def 2;

( 0 = 0 + 1 or 1 = 0 + 1 ) ;

then [0,1] in the InternalRel of (Necklace 4) by A12, A13, NECKLACE:25;

then A14: [(f . 0),(f . 1)] in the InternalRel of S by A10, A12, A13;

then A15: f . 1 in rng the InternalRel of S by XTUPLE_0:def 13;

f . 0 in dom the InternalRel of S by A14, XTUPLE_0:def 12;

then f . 0 = f . 1 by A7, A15, A8, A9, STRUCT_0:def 10;

then [0,0] in the InternalRel of (Necklace 4) by A10, A12, A14;

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 Th2, ENUMSET1:def 4;

hence ex n being Nat st

( n < m & S_{1}[n] )
by XTUPLE_0:1; :: thesis: verum

end;A9: rng the InternalRel of S c= the carrier of S by RELAT_1:def 19;

consider f being Function of (Necklace 4),S such that

f is one-to-one and

A10: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

A11: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;

then A12: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A13: 1 in the carrier of (Necklace 4) by A11, ENUMSET1:def 2;

( 0 = 0 + 1 or 1 = 0 + 1 ) ;

then [0,1] in the InternalRel of (Necklace 4) by A12, A13, NECKLACE:25;

then A14: [(f . 0),(f . 1)] in the InternalRel of S by A10, A12, A13;

then A15: f . 1 in rng the InternalRel of S by XTUPLE_0:def 13;

f . 0 in dom the InternalRel of S by A14, XTUPLE_0:def 12;

then f . 0 = f . 1 by A7, A15, A8, A9, STRUCT_0:def 10;

then [0,0] in the InternalRel of (Necklace 4) by A10, A12, A14;

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 Th2, ENUMSET1:def 4;

hence ex n being Nat st

( n < m & S

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 & S_{1}[n] )

( 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 & S

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) ) ;

( n < m & S_{1}[n] )
by A19, A20; :: thesis: verum

end;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 & S_{1}[n] ) )

( n < m & S

A21:
not [1,3] in the InternalRel of (Necklace 4)

then A26: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A27: not [0,3] in the InternalRel of (Necklace 4)

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 & S_{1}[n] )

A31: [: the carrier of H1, the carrier of H2:] c= the InternalRel of S

A34: 3 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

A35: [: the carrier of H2, the carrier of H1:] c= the InternalRel of S

A38: 1 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

consider f being Function of (Necklace 4),S such that

A39: f is one-to-one and

A40: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A41: [(f . 1),(f . 0)] in the InternalRel of S by A40, A26, A38;

A42: 2 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A43: [(f . 3),(f . 2)] in the InternalRel of S by A40, A42, A34;

[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A44: [(f . 2),(f . 1)] in the InternalRel of S by A40, A38, A42;

A45: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;

[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A46: [(f . 2),(f . 3)] in the InternalRel of S by A40, A42, A34;

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 A30, Def3;

[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A48: [(f . 0),(f . 1)] in the InternalRel of S by A40, A26, A38;

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 A30, Def3;

f . 1 in rng the InternalRel of S by A48, XTUPLE_0:def 13;

then f . 1 in the carrier of S by A33;

then A50: f . 1 in the carrier of H1 \/ the carrier of H2 by A30, Def3;

A51: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;

[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A52: [(f . 1),(f . 2)] in the InternalRel of S by A40, A38, A42;

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 A30, Def3;

A54: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;

end;proof

A23:
not [0,2] in the InternalRel of (Necklace 4)
assume A22:
[1,3] in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;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 A22, Th2, ENUMSET1:def 4;

end;

proof

A25:
the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:1, NECKLACE:20;
assume A24:
[0,2] in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;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 A24, Th2, ENUMSET1:def 4;

end;

then A26: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A27: not [0,3] in the InternalRel of (Necklace 4)

proof

set A = the InternalRel of H1;
assume A28:
[0,3] in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;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 A28, Th2, ENUMSET1:def 4;

end;

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 & S

A31: [: the carrier of H1, the carrier of H2:] c= the InternalRel of S

proof

A33:
rng the InternalRel of S c= the carrier of S
by RELAT_1:def 19;
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 A30, Def3;

hence x in the InternalRel of S by A32; :: thesis: verum

end;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 A30, Def3;

hence x in the InternalRel of S by A32; :: thesis: verum

A34: 3 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

A35: [: the carrier of H2, the carrier of H1:] c= the InternalRel of S

proof

A37:
rng the InternalRel of H1 c= the carrier of H1
by RELAT_1:def 19;
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 A30, Def3;

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;( 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 A30, Def3;

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

A38: 1 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

consider f being Function of (Necklace 4),S such that

A39: f is one-to-one and

A40: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A41: [(f . 1),(f . 0)] in the InternalRel of S by A40, A26, A38;

A42: 2 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;

[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A43: [(f . 3),(f . 2)] in the InternalRel of S by A40, A42, A34;

[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A44: [(f . 2),(f . 1)] in the InternalRel of S by A40, A38, A42;

A45: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;

[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A46: [(f . 2),(f . 3)] in the InternalRel of S by A40, A42, A34;

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 A30, Def3;

[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A48: [(f . 0),(f . 1)] in the InternalRel of S by A40, A26, A38;

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 A30, Def3;

f . 1 in rng the InternalRel of S by A48, XTUPLE_0:def 13;

then f . 1 in the carrier of S by A33;

then A50: f . 1 in the carrier of H1 \/ the carrier of H2 by A30, Def3;

A51: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;

[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A52: [(f . 1),(f . 2)] in the InternalRel of S by A40, A38, A42;

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 A30, Def3;

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 A49, XBOOLE_0:def 3;

end;

suppose A55:
f . 0 in the carrier of H1
; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

( n < m & S

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)];

rng f c= the carrier of H1

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A68: H1 is non empty strict RelStr by A17, Th4;

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 A58, A59, A63, XBOOLE_0:def 3, ZFMISC_1:87;

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 A72, A57, A63, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A43, Def3;

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 A69, A57, A61, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A46, Def3;

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 A70, A61, A57, XBOOLE_0:def 3, ZFMISC_1:87;

then reconsider cH2 = the carrier of H2 as finite set ;

the carrier of S = cH1 \/ cH2 by A30, Def3;

then reconsider cS = the carrier of S as finite set ;

A77: not H2 is empty by A18, Th4;

A78: cH1 <> cS

then cH1 c= cS by XBOOLE_1:7;

then cH1 c< cS by A78, XBOOLE_0:def 8;

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 A30, A44, Def3;

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 A76, A63, A57, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A48, Def3;

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 A60, A63, A56, XBOOLE_0:def 3, ZFMISC_1:87;

for x, y being Element of (Necklace 4) holds

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

hence ex n being Nat st

( n < m & S_{1}[n] )
by A5, A17, A68, A82; :: thesis: verum

end;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;then f . 0 in the carrier of H2 by ZFMISC_1:87;

hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum

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 A55, ZFMISC_1:87;

hence contradiction by A40, A26, A42, A23, A31; :: thesis: verum

end;then [(f . 0),(f . 2)] in [: the carrier of H1, the carrier of H2:] by A55, ZFMISC_1:87;

hence contradiction by A40, A26, A42, A23, A31; :: thesis: verum

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;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

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;then f . 0 in the carrier of H2 by ZFMISC_1:87;

hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum

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;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

A61: now :: thesis: not f . 3 in the carrier of H2

then A62:
f . 3 in the carrier of H1
by A47, XBOOLE_0:def 3;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 A55, ZFMISC_1:87;

hence contradiction by A40, A26, A34, A27, A31; :: thesis: verum

end;then [(f . 0),(f . 3)] in [: the carrier of H1, the carrier of H2:] by A55, ZFMISC_1:87;

hence contradiction by A40, A26, A34, A27, A31; :: thesis: verum

A63: now :: thesis: not f . 1 in the carrier of H2

A64:
dom f = the carrier of (Necklace 4)
by FUNCT_2:def 1;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 A62, ZFMISC_1:87;

hence contradiction by A40, A38, A34, A21, A35; :: thesis: verum

end;then [(f . 1),(f . 3)] in [: the carrier of H2, the carrier of H1:] by A62, ZFMISC_1:87;

hence contradiction by A40, A38, A34, A21, A35; :: thesis: verum

rng f c= the carrier of H1

proof

then A67:
f is Function of the carrier of (Necklace 4), the carrier of H1
by FUNCT_2:6;
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;

end;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;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A68: H1 is non empty strict RelStr by A17, Th4;

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;then f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;

hence contradiction by A45, A57; :: thesis: verum

A70: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H2

[(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 A30, A41, Def3;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;then f . 2 in dom the InternalRel of H2 by XTUPLE_0:def 12;

hence contradiction by A54, A57; :: thesis: verum

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 A58, A59, A63, XBOOLE_0:def 3, ZFMISC_1:87;

A72: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2

[(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 A30, A52, Def3;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;then f . 1 in dom the InternalRel of H2 by XTUPLE_0:def 12;

hence contradiction by A54, A63; :: thesis: verum

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 A72, A57, A63, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A43, Def3;

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 A69, A57, A61, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A46, Def3;

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 A70, A61, A57, XBOOLE_0:def 3, ZFMISC_1:87;

A76: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H2

H2 is finite
by A18, Th4;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;then f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;

hence contradiction by A45, A63; :: thesis: verum

then reconsider cH2 = the carrier of H2 as finite set ;

the carrier of S = cH1 \/ cH2 by A30, Def3;

then reconsider cS = the carrier of S as finite set ;

A77: not H2 is empty by A18, Th4;

A78: cH1 <> cS

proof

cS = cH1 \/ cH2
by A30, Def3;
A79:
cS = cH1 \/ cH2
by A30, Def3;

assume A80: cH1 = cS ; :: thesis: contradiction

consider x being object such that

A81: x in cH2 by A77, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH1 by A81, XBOOLE_0:def 4;

hence contradiction by A80, A79, A81, XBOOLE_0:def 3; :: thesis: verum

end;assume A80: cH1 = cS ; :: thesis: contradiction

consider x being object such that

A81: x in cH2 by A77, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH1 by A81, XBOOLE_0:def 4;

hence contradiction by A80, A79, A81, XBOOLE_0:def 3; :: thesis: verum

then cH1 c= cS by XBOOLE_1:7;

then cH1 c< cS by A78, XBOOLE_0:def 8;

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 A30, A44, Def3;

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 A76, A63, A57, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A48, Def3;

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 A60, A63, A56, XBOOLE_0:def 3, ZFMISC_1:87;

for x, y being Element of (Necklace 4) holds

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

proof

then
H1 embeds Necklace 4
by A39, A67, NECKLACE:def 1;
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 H1 )

thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

proof

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

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 A85, Th2, ENUMSET1:def 4;

end;

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 A84, A86, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A84, A86, XTUPLE_0:1; :: thesis: verum

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 A71, A87, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A71, A87, XTUPLE_0:1; :: thesis: verum

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 A73, A88, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A73, A88, XTUPLE_0:1; :: thesis: verum

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 A83, A89, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A83, A89, XTUPLE_0:1; :: thesis: verum

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 A75, A90, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A75, A90, XTUPLE_0:1; :: thesis: verum

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 A74, A91, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A74, A91, XTUPLE_0:1; :: thesis: verum

proof

( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) )
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 (Necklace 4) ) by A30, Def3;

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 (Necklace 4) ) 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 (Necklace 4) ) by XBOOLE_1:4;

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

hence [x,y] in the InternalRel of (Necklace 4) by A92, XBOOLE_0:def 3; :: thesis: verum

end;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 (Necklace 4) ) by A30, Def3;

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 (Necklace 4) ) 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 (Necklace 4) ) by XBOOLE_1:4;

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

hence [x,y] in the InternalRel of (Necklace 4) by A92, XBOOLE_0:def 3; :: thesis: verum

hence ex n being Nat st

( n < m & S

suppose A93:
f . 0 in the carrier of H2
; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

( n < m & S

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)];

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 A99, A98, A95, XBOOLE_0:def 3, ZFMISC_1:87;

rng f c= the carrier of H2

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A107: H2 is non empty strict RelStr by A18, Th4;

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 A109, A96, A102, XBOOLE_0:def 3, ZFMISC_1:87;

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 A112, A98, A102, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A46, Def3;

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 A110, A102, A96, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A44, Def3;

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 A101, A102, A98, XBOOLE_0:def 3, ZFMISC_1:87;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

the carrier of S = cH1 \/ cH2 by A30, Def3;

then reconsider cS = the carrier of S as finite set ;

A116: not H1 is empty by A17, Th4;

A117: cH2 <> cS

then cH2 c= cS by XBOOLE_1:7;

then cH2 c< cS by A117, XBOOLE_0:def 8;

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 A30, A48, Def3;

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 A108, A94, A98, XBOOLE_0:def 3, ZFMISC_1:87;

for x, y being Element of (Necklace 4) holds

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

hence ex n being Nat st

( n < m & S_{1}[n] )
by A5, A18, A107, A121; :: thesis: verum

end;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;then f . 0 in the carrier of H1 by ZFMISC_1:87;

hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum

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;then f . 0 in the carrier of H1 by ZFMISC_1:87;

hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum

A96: now :: thesis: not f . 3 in the carrier of H1

then A97:
f . 3 in the carrier of H2
by A47, XBOOLE_0:def 3;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 A93, ZFMISC_1:87;

hence contradiction by A40, A26, A34, A27, A35; :: thesis: verum

end;then [(f . 0),(f . 3)] in [: the carrier of H2, the carrier of H1:] by A93, ZFMISC_1:87;

hence contradiction by A40, A26, A34, A27, A35; :: thesis: verum

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 A97, ZFMISC_1:87;

hence contradiction by A40, A38, A34, A21, A31; :: thesis: verum

end;then [(f . 1),(f . 3)] in [: the carrier of H1, the carrier of H2:] by A97, ZFMISC_1:87;

hence contradiction by A40, A38, A34, A21, A31; :: thesis: verum

A99: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1

[(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 A30, A41, Def3;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;then f . 1 in dom the InternalRel of H1 by XTUPLE_0:def 12;

hence contradiction by A51, A98; :: thesis: verum

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 A99, A98, A95, XBOOLE_0:def 3, ZFMISC_1:87;

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;then f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;

hence contradiction by A37, A98; :: thesis: verum

A102: now :: thesis: not f . 2 in the carrier of H1

A103:
dom f = the carrier of (Necklace 4)
by FUNCT_2:def 1;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 A93, ZFMISC_1:87;

hence contradiction by A40, A26, A42, A23, A35; :: thesis: verum

end;then [(f . 0),(f . 2)] in [: the carrier of H2, the carrier of H1:] by A93, ZFMISC_1:87;

hence contradiction by A40, A26, A42, A23, A35; :: thesis: verum

rng f c= the carrier of H2

proof

then A106:
f is Function of the carrier of (Necklace 4), the carrier of H2
by FUNCT_2:6;
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;

end;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;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A107: H2 is non empty strict RelStr by A18, Th4;

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;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

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;then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;

hence contradiction by A37, A102; :: thesis: verum

A110: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H1

[(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 A30, A43, Def3;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;then f . 2 in dom the InternalRel of H1 by XTUPLE_0:def 12;

hence contradiction by A51, A102; :: thesis: verum

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 A109, A96, A102, XBOOLE_0:def 3, ZFMISC_1:87;

A112: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1

[(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 A30, A52, Def3;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;then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;

hence contradiction by A37, A102; :: thesis: verum

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 A112, A98, A102, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A46, Def3;

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 A110, A102, A96, XBOOLE_0:def 3, ZFMISC_1:87;

[(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 A30, A44, Def3;

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 A101, A102, A98, XBOOLE_0:def 3, ZFMISC_1:87;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

the carrier of S = cH1 \/ cH2 by A30, Def3;

then reconsider cS = the carrier of S as finite set ;

A116: not H1 is empty by A17, Th4;

A117: cH2 <> cS

proof

cS = cH1 \/ cH2
by A30, Def3;
A118:
cS = cH1 \/ cH2
by A30, Def3;

assume A119: cH2 = cS ; :: thesis: contradiction

consider x being object such that

A120: x in cH1 by A116, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH2 by A120, XBOOLE_0:def 4;

hence contradiction by A119, A118, A120, XBOOLE_0:def 3; :: thesis: verum

end;assume A119: cH2 = cS ; :: thesis: contradiction

consider x being object such that

A120: x in cH1 by A116, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH2 by A120, XBOOLE_0:def 4;

hence contradiction by A119, A118, A120, XBOOLE_0:def 3; :: thesis: verum

then cH2 c= cS by XBOOLE_1:7;

then cH2 c< cS by A117, XBOOLE_0:def 8;

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 A30, A48, Def3;

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 A108, A94, A98, XBOOLE_0:def 3, ZFMISC_1:87;

for x, y being Element of (Necklace 4) holds

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

proof

then
H2 embeds Necklace 4
by A39, A106, NECKLACE:def 1;
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 H2 )

thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

proof

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

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 A123, Th2, ENUMSET1:def 4;

end;

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 A122, A124, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A122, A124, XTUPLE_0:1; :: thesis: verum

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 A100, A125, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A100, A125, XTUPLE_0:1; :: thesis: verum

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 A113, A126, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A113, A126, XTUPLE_0:1; :: thesis: verum

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 A115, A127, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A115, A127, XTUPLE_0:1; :: thesis: verum

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 A114, A128, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A114, A128, XTUPLE_0:1; :: thesis: verum

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 A111, A129, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A111, A129, XTUPLE_0:1; :: thesis: verum

proof

( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) )
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 (Necklace 4) ) by A30, Def3;

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 (Necklace 4) ) 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 (Necklace 4) ) by XBOOLE_1:4;

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

hence [x,y] in the InternalRel of (Necklace 4) by A130, XBOOLE_0:def 3; :: thesis: verum

end;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 (Necklace 4) ) by A30, Def3;

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 (Necklace 4) ) 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 (Necklace 4) ) by XBOOLE_1:4;

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

hence [x,y] in the InternalRel of (Necklace 4) by A130, XBOOLE_0:def 3; :: thesis: verum

hence ex n being Nat st

( n < m & S

now :: thesis: ( S = union_of (H1,H2) implies ex n being Nat st

( n < m & S_{1}[n] ) )

hence
ex n being Nat st ( n < m & S

A131:
the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:1, NECKLACE:20;

then A132: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A133: 3 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

A134: 1 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

A135: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;

consider f being Function of (Necklace 4),S such that

A136: f is one-to-one and

A137: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

assume A138: S = union_of (H1,H2) ; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A139: [(f . 0),(f . 1)] in the InternalRel of S by A137, A132, A134;

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 A138, Def2;

A141: 2 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A142: [(f . 3),(f . 2)] in the InternalRel of S by A137, A141, A133;

[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A143: [(f . 2),(f . 3)] in the InternalRel of S by A137, A141, A133;

[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A144: [(f . 2),(f . 1)] in the InternalRel of S by A137, A134, A141;

[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A145: [(f . 1),(f . 2)] in the InternalRel of S by A137, A134, A141;

[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A146: [(f . 1),(f . 0)] in the InternalRel of S by A137, A132, A134;

end;then A132: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A133: 3 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

A134: 1 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

A135: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;

consider f being Function of (Necklace 4),S such that

A136: f is one-to-one and

A137: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of S ) by A6, NECKLACE:def 1;

assume A138: S = union_of (H1,H2) ; :: thesis: ex n being Nat st

( n < m & S

[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A139: [(f . 0),(f . 1)] in the InternalRel of S by A137, A132, A134;

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 A138, Def2;

A141: 2 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;

[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A142: [(f . 3),(f . 2)] in the InternalRel of S by A137, A141, A133;

[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A143: [(f . 2),(f . 3)] in the InternalRel of S by A137, A141, A133;

[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A144: [(f . 2),(f . 1)] in the InternalRel of S by A137, A134, A141;

[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A145: [(f . 1),(f . 2)] in the InternalRel of S by A137, A134, A141;

[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;

then A146: [(f . 1),(f . 0)] in the InternalRel of S by A137, A132, A134;

per cases
( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 )
by A140, XBOOLE_0:def 3;

end;

suppose A147:
f . 0 in the carrier of H1
; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

( n < m & S

set cS = the carrier of S;

set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

A148: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A149: the carrier of S = cH1 \/ cH2 by A138, Def2;

A150: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;

then A154: [(f . 1),(f . 0)] in the InternalRel of H1 by A153, XBOOLE_0:def 3;

A155: H1 is non empty strict RelStr by A17, Th4;

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 A138, A139, Def2;

then A157: [(f . 0),(f . 1)] in the InternalRel of H1 by A151, XBOOLE_0:def 3;

then A158: f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;

A161: cH1 <> cS

then cH1 c= cS by XBOOLE_1:7;

then cH1 c< cS by A161, XBOOLE_0:def 8;

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 A138, A143, Def2;

A167: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;

then A169: f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;

[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;

then A171: [(f . 2),(f . 1)] in the InternalRel of H1 by A159, XBOOLE_0:def 3;

then A173: [(f . 3),(f . 2)] in the InternalRel of H1 by A172, XBOOLE_0:def 3;

A174: for x, y being Element of (Necklace 4) holds

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

rng f c= the carrier of H1

then H1 embeds Necklace 4 by A136, A174, NECKLACE:def 1;

hence ex n being Nat st

( n < m & S_{1}[n] )
by A5, A17, A155, A165; :: thesis: verum

end;set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

A148: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A149: the carrier of S = cH1 \/ cH2 by A138, Def2;

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

A152:
rng the InternalRel of H2 c= the carrier of H2
by RELAT_1:def 19;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;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

A153: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H2

[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2
by A138, A146, Def2;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;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

then A154: [(f . 1),(f . 0)] in the InternalRel of H1 by A153, XBOOLE_0:def 3;

A155: H1 is non empty strict RelStr by A17, Th4;

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 A138, A139, Def2;

then A157: [(f . 0),(f . 1)] in the InternalRel of H1 by A151, XBOOLE_0:def 3;

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

A160:
not H2 is empty
by A18, Th4;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;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

A161: cH1 <> cS

proof

cS = cH1 \/ cH2
by A138, Def2;
A162:
cS = cH1 \/ cH2
by A138, Def2;

assume A163: cH1 = cS ; :: thesis: contradiction

consider x being object such that

A164: x in cH2 by A160, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH1 by A164, XBOOLE_0:def 4;

hence contradiction by A163, A162, A164, XBOOLE_0:def 3; :: thesis: verum

end;assume A163: cH1 = cS ; :: thesis: contradiction

consider x being object such that

A164: x in cH2 by A160, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH1 by A164, XBOOLE_0:def 4;

hence contradiction by A163, A162, A164, XBOOLE_0:def 3; :: thesis: verum

then cH1 c= cS by XBOOLE_1:7;

then cH1 c< cS by A161, XBOOLE_0:def 8;

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 A138, A143, Def2;

A167: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;

now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2

then A168:
[(f . 1),(f . 2)] in the InternalRel of H1
by A167, XBOOLE_0:def 3;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 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

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

then A170:
[(f . 2),(f . 3)] in the InternalRel of H1
by A166, XBOOLE_0:def 3;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 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

[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;

then A171: [(f . 2),(f . 1)] in the InternalRel of H1 by A159, XBOOLE_0:def 3;

A172: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H2

[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2
by A138, A142, Def2;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;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

then A173: [(f . 3),(f . 2)] in the InternalRel of H1 by A172, XBOOLE_0:def 3;

A174: for x, y being Element of (Necklace 4) holds

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

proof

A183:
f . 3 in rng the InternalRel of H1
by A170, XTUPLE_0:def 13;
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 H1 )

thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

proof

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

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 A175, Th2, ENUMSET1:def 4;

end;

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 A157, A176, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A157, A176, XTUPLE_0:1; :: thesis: verum

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 A154, A177, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A154, A177, XTUPLE_0:1; :: thesis: verum

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 A168, A178, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A168, A178, XTUPLE_0:1; :: thesis: verum

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 A171, A179, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A171, A179, XTUPLE_0:1; :: thesis: verum

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 A170, A180, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A170, A180, XTUPLE_0:1; :: thesis: verum

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 A173, A181, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H1 by A173, A181, XTUPLE_0:1; :: thesis: verum

proof

( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) )
by A137;

then A182: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;

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

hence [x,y] in the InternalRel of (Necklace 4) by A182, XBOOLE_0:def 3; :: thesis: verum

end;then A182: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;

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

hence [x,y] in the InternalRel of (Necklace 4) by A182, XBOOLE_0:def 3; :: thesis: verum

rng f c= the carrier of H1

proof

then
f is Function of the carrier of (Necklace 4), the carrier of H1
by FUNCT_2:6;
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;

end;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;

then H1 embeds Necklace 4 by A136, A174, NECKLACE:def 1;

hence ex n being Nat st

( n < m & S

suppose A186:
f . 0 in the carrier of H2
; :: thesis: ex n being Nat st

( n < m & S_{1}[n] )

( n < m & S

set cS = the carrier of S;

set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

A187: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A188: the carrier of S = cH1 \/ cH2 by A138, Def2;

A189: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;

then A193: [(f . 1),(f . 0)] in the InternalRel of H2 by A192, XBOOLE_0:def 3;

A194: H2 is non empty strict RelStr by A18, Th4;

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 A138, A139, Def2;

then A196: [(f . 0),(f . 1)] in the InternalRel of H2 by A190, XBOOLE_0:def 3;

then A197: f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;

A200: cH2 <> cS

then cH2 c= cS by XBOOLE_1:7;

then cH2 c< cS by A200, XBOOLE_0:def 8;

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 A138, A143, Def2;

A206: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;

then A208: f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;

[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;

then A210: [(f . 2),(f . 1)] in the InternalRel of H2 by A198, XBOOLE_0:def 3;

then A212: [(f . 3),(f . 2)] in the InternalRel of H2 by A211, XBOOLE_0:def 3;

A213: for x, y being Element of (Necklace 4) holds

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

rng f c= the carrier of H2

then H2 embeds Necklace 4 by A136, A213, NECKLACE:def 1;

hence ex n being Nat st

( n < m & S_{1}[n] )
by A5, A18, A194, A204; :: thesis: verum

end;set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

A187: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

H2 is finite by A18, Th4;

then reconsider cH2 = the carrier of H2 as finite set ;

H1 is finite by A17, Th4;

then reconsider cH1 = the carrier of H1 as finite set ;

A188: the carrier of S = cH1 \/ cH2 by A138, Def2;

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

A191:
rng the InternalRel of H1 c= the carrier of H1
by RELAT_1:def 19;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;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

A192: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1

[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2
by A138, A146, Def2;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;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

then A193: [(f . 1),(f . 0)] in the InternalRel of H2 by A192, XBOOLE_0:def 3;

A194: H2 is non empty strict RelStr by A18, Th4;

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 A138, A139, Def2;

then A196: [(f . 0),(f . 1)] in the InternalRel of H2 by A190, XBOOLE_0:def 3;

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

A199:
not H1 is empty
by A17, Th4;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;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

A200: cH2 <> cS

proof

cS = cH1 \/ cH2
by A138, Def2;
A201:
cS = cH1 \/ cH2
by A138, Def2;

assume A202: cH2 = cS ; :: thesis: contradiction

consider x being object such that

A203: x in cH1 by A199, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH2 by A203, XBOOLE_0:def 4;

hence contradiction by A202, A201, A203, XBOOLE_0:def 3; :: thesis: verum

end;assume A202: cH2 = cS ; :: thesis: contradiction

consider x being object such that

A203: x in cH1 by A199, XBOOLE_0:def 1;

cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;

then not x in cH2 by A203, XBOOLE_0:def 4;

hence contradiction by A202, A201, A203, XBOOLE_0:def 3; :: thesis: verum

then cH2 c= cS by XBOOLE_1:7;

then cH2 c< cS by A200, XBOOLE_0:def 8;

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 A138, A143, Def2;

A206: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;

now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1

then A207:
[(f . 1),(f . 2)] in the InternalRel of H2
by A206, XBOOLE_0:def 3;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 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

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

then A209:
[(f . 2),(f . 3)] in the InternalRel of H2
by A205, XBOOLE_0:def 3;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 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

[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;

then A210: [(f . 2),(f . 1)] in the InternalRel of H2 by A198, XBOOLE_0:def 3;

A211: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H1

[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2
by A138, A142, Def2;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;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

then A212: [(f . 3),(f . 2)] in the InternalRel of H2 by A211, XBOOLE_0:def 3;

A213: for x, y being Element of (Necklace 4) holds

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

proof

A222:
f . 3 in rng the InternalRel of H2
by A209, XTUPLE_0:def 13;
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 H2 )

thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) 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 (Necklace 4) )

proof

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

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 A214, Th2, ENUMSET1:def 4;

end;

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 A196, A215, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A196, A215, XTUPLE_0:1; :: thesis: verum

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 A193, A216, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A193, A216, XTUPLE_0:1; :: thesis: verum

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 A207, A217, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A207, A217, XTUPLE_0:1; :: thesis: verum

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 A210, A218, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A210, A218, XTUPLE_0:1; :: thesis: verum

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 A209, A219, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A209, A219, XTUPLE_0:1; :: thesis: verum

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 A212, A220, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of H2 by A212, A220, XTUPLE_0:1; :: thesis: verum

proof

( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) )
by A137;

then A221: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;

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

hence [x,y] in the InternalRel of (Necklace 4) by A221, XBOOLE_0:def 3; :: thesis: verum

end;then A221: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;

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

hence [x,y] in the InternalRel of (Necklace 4) by A221, XBOOLE_0:def 3; :: thesis: verum

rng f c= the carrier of H2

proof

then
f is Function of the carrier of (Necklace 4), the carrier of H2
by FUNCT_2:6;
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;

end;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;

then H2 embeds Necklace 4 by A136, A213, NECKLACE:def 1;

hence ex n being Nat st

( n < m & S

( n < m & S

then S

then A225: ex i being Nat st S

S

hence contradiction ; :: thesis: verum