:: NECKLA_2 semantic presentation

begin

theorem Th1: :: NECKLA_2:1
for U being Universe
for X, Y being set st X in U & Y in U holds
for R being Relation of X,Y holds R in U
proof
let U be Universe; ::_thesis: for X, Y being set st X in U & Y in U holds
for R being Relation of X,Y holds R in U
let X, Y be set ; ::_thesis: ( X in U & Y in U implies for R being Relation of X,Y holds R in U )
assume that
A1: X in U and
A2: Y in U ; ::_thesis: for R being Relation of X,Y holds R in U
 [:X,Y:] in U by A1, A2, CLASSES2:61;
hence  for R being Relation of X,Y holds R in U by CLASSES1:def_1; ::_thesis: verum
end;

theorem Th2: :: NECKLA_2:2
the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
proof
set A = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]};
set B = the InternalRel of (Necklace 4);
A1: [(0 + 1),0] in  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  ;
A2: the InternalRel of (Necklace 4) =  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  \/  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  by NECKLACE:18;
A3: the InternalRel of (Necklace 4) c= {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of (Necklace 4) or x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} )
assume A4: x in the InternalRel of (Necklace 4) ; ::_thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
then consider y, z being set  such that
A5: x = [y,z] by RELAT_1:def_1;
percases ( x in  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  or x in  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  ) by A2, A4, XBOOLE_0:def_3;
suppose x in  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  ; ::_thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
then consider i being Element of NAT  such that
A6: [y,z] = [i,(i + 1)] and
A7: i + 1 < 4 by A5;
A8: y = i by A6, XTUPLE_0:1;
 i + 1 < 1 + 3 by A7;
then  i < 2 + 1 by XREAL_1:7;
then  i <= 2 by NAT_1:13;
then  ( y = 0 or y = 1 or y = 2 ) by A8, NAT_1:26;
hence  x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A5, A6, A8, ENUMSET1:def_4; ::_thesis: verum
end;
suppose x in  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  ; ::_thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
then consider i being Element of NAT  such that
A9: [y,z] = [(i + 1),i] and
A10: i + 1 < 4 by A5;
A11: z = i by A9, XTUPLE_0:1;
 i + 1 < 1 + 3 by A10;
then  i < 2 + 1 by XREAL_1:7;
then  i <= 2 by NAT_1:13;
then  ( z = 0 or z = 1 or z = 2 ) by A11, NAT_1:26;
hence  x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A5, A9, A11, ENUMSET1:def_4; ::_thesis: verum
end;
end;
end;
A12: [(2 + 1),(1 + 1)] in  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  ;
A13: [(1 + 1),(2 + 1)] in  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  ;
A14: [(1 + 1),(0 + 1)] in  {  [(i + 1),i] where i is Element of NAT : i + 1 < 4  }  ;
A15: [(0 + 1),(1 + 1)] in  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  ;
A16: [0,(0 + 1)] in  {  [i,(i + 1)] where i is Element of NAT : i + 1 < 4  }  ;
 {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} c= the InternalRel of (Necklace 4)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} or x in the InternalRel of (Necklace 4) )
assume A17: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} ; ::_thesis: x in the InternalRel of (Necklace 4)
percases ( x = [0,1] or x = [1,0] or x = [1,2] or x = [2,1] or x = [2,3] or x = [3,2] ) by A17, ENUMSET1:def_4;
suppose x = [0,1] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A16, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = [1,0] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = [1,2] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = [2,1] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A14, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = [2,3] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A13, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = [3,2] ; ::_thesis: x in the InternalRel of (Necklace 4)
hence  x in the InternalRel of (Necklace 4) by A2, A12, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let n be Nat;
cluster  ->  finite for Element of Rank n;
coherence
 for b1 being Element of Rank n holds b1 is finite
proof
reconsider m = n as Element of NAT by ORDINAL1:def_12;
let x be Element of Rank n; ::_thesis: x is finite
percases ( Rank n = {} or Rank n <> {} ) ;
suppose Rank n = {} ; ::_thesis: x is finite
hence  x is finite ; ::_thesis: verum
end;
supposeA1: Rank n <> {} ; ::_thesis: x is finite
A2: Rank m is finite by CARD_2:67;
 x c= Rank n by A1, ORDINAL1:def_2;
hence  x is finite by A2; ::_thesis: verum
end;
end;
end;
end;

theorem Th3: :: NECKLA_2:3
for x being set st x in FinSETS holds
x is finite
proof
A1: omega is limit_ordinal by ORDINAL1:def_11;
let x be set ; ::_thesis: ( x in FinSETS implies x is finite )
assume  x in FinSETS ; ::_thesis: x is finite
then consider n being Ordinal such that
A2: n in omega and
A3: x in Rank n by A1, CLASSES1:31, CLASSES2:64;
reconsider n = n as Nat by A2;
 x is Element of Rank n by A3;
hence  x is finite ; ::_thesis: verum
end;

registration
cluster  ->  finite for Element of FinSETS ;
coherence
 for b1 being Element of FinSETS holds b1 is finite by Th3;
end;

definition
let G be non empty RelStr ;
attrG is N-free  means :Def1: :: NECKLA_2:def 1
 not G embeds Necklace 4;
end;

:: deftheorem Def1 defines N-free NECKLA_2:def_1_:_
 for G being non empty RelStr holds
( G is N-free iff not G embeds Necklace 4 );

registration
cluster non empty finite strict N-free for RelStr ;
existence
 ex b1 being non empty RelStr st
( b1 is strict & b1 is finite & b1 is N-free )
proof
set X = {0,1};
set Y = Necklace 4;
reconsider r = id {0,1} as Relation of {0,1} by RELSET_1:14;
take R = RelStr(# {0,1},r #); ::_thesis: ( R is strict & R is finite & R is N-free )
now__::_thesis:_for_f_being_Function_of_(Necklace_4),R_st_f_is_one-to-one_holds_
ex_x,_y_being_Element_of_(Necklace_4)_st_
(_(_[x,y]_in_the_InternalRel_of_(Necklace_4)_implies_[(f_._x),(f_._y)]_in_the_InternalRel_of_R_)_implies_(_[(f_._x),(f_._y)]_in_the_InternalRel_of_R_&_not_[x,y]_in_the_InternalRel_of_(Necklace_4)_)_)
let f be Function of (Necklace 4),R; ::_thesis: ( f is one-to-one implies ex x, y being Element of (Necklace 4) st
( ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of R ) implies ( [(f . x),(f . y)] in the InternalRel of R & not [x,y] in the InternalRel of (Necklace 4) ) ) )
A1: dom f = the carrier of (Necklace 4) by FUNCT_2:def_1
.= {0,1,2,3} by NECKLACE:1, NECKLACE:20 ;
then A2: 3 in dom f by ENUMSET1:def_2;
then A3: f . 3 in {0,1} by PARTFUN1:4;
A4: 2 in dom f by A1, ENUMSET1:def_2;
then  f . 2 in {0,1} by PARTFUN1:4;
then A5: ( f . 2 = 0 or f . 2 = 1 ) by TARSKI:def_2;
A6: 1 in dom f by A1, ENUMSET1:def_2;
then  f . 1 in {0,1} by PARTFUN1:4;
then A7: ( f . 1 = 0 or f . 1 = 1 ) by TARSKI:def_2;
assume A8: f is one-to-one ; ::_thesis: not 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 R )
then A9: f . 2 <> f . 3 by A4, A2, FUNCT_1:def_4;
 f . 1 <> f . 3 by A8, A6, A2, FUNCT_1:def_4;
hence  not 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 R ) by A8, A6, A4, A9, A3, A7, A5, FUNCT_1:def_4, TARSKI:def_2; ::_thesis: verum
end;
then  not R embeds Necklace 4 by NECKLACE:def_1;
hence  ( R is strict & R is finite & R is N-free ) by Def1; ::_thesis: verum
end;
end;

definition
let R, S be RelStr ;
func union_of (R,S) ->  strict RelStr  means :Def2: :: NECKLA_2:def 2
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = the InternalRel of R \/ the InternalRel of S );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = the InternalRel of R \/ the InternalRel of S )
proof
set X = the carrier of R \/ the carrier of S;
A1: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
 the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by A1, RELSET_1:7;
set D = IR \/ IS;
reconsider D = IR \/ IS as Relation of ( the carrier of R \/ the carrier of S) ;
take  RelStr(# ( the carrier of R \/ the carrier of S),D #) ; ::_thesis: ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),D #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),D #) = the InternalRel of R \/ the InternalRel of S )
thus  ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),D #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),D #) = the InternalRel of R \/ the InternalRel of S ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = the InternalRel of R \/ the InternalRel of S & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = the InternalRel of R \/ the InternalRel of S holds
b1 = b2 ;
end;

:: deftheorem Def2 defines union_of NECKLA_2:def_2_:_
 for R, S being RelStr
for b3 being strict RelStr holds
( b3 = union_of (R,S) iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = the InternalRel of R \/ the InternalRel of S ) );

definition
let R, S be RelStr ;
func sum_of (R,S) ->  strict RelStr  means :Def3: :: NECKLA_2:def 3
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] )
proof
set X = the carrier of R \/ the carrier of S;
A1: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
A2: the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
then reconsider IQ = [: the carrier of R, the carrier of S:] as Relation of ( the carrier of R \/ the carrier of S) by A1, ZFMISC_1:96;
reconsider IP = [: the carrier of S, the carrier of R:] as Relation of ( the carrier of R \/ the carrier of S) by A2, A1, ZFMISC_1:96;
A3: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
 the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by A3, RELSET_1:7;
set D = ((IR \/ IS) \/ IQ) \/ IP;
take  RelStr(# ( the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) ; ::_thesis: ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] )
thus  ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] holds
b1 = b2 ;
end;

:: deftheorem Def3 defines sum_of NECKLA_2:def_3_:_
 for R, S being RelStr
for b3 being strict RelStr holds
( b3 = sum_of (R,S) iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] ) );

definition
func fin_RelStr  ->  set  means :Def4: :: NECKLA_2:def 4
 for X being set holds
( X in it iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) );
existence
 ex b1 being set st
for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
proof
defpred S1[ set , set ] means  ex R being strict RelStr st
( $1 = [ the carrier of R, the InternalRel of R] & $2 = R );
A1: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z )
given R1 being strict RelStr  such that A2: x = [ the carrier of R1, the InternalRel of R1] and
A3: y = R1 ; ::_thesis: ( not S1[x,z] or y = z )
given R2 being strict RelStr  such that A4: x = [ the carrier of R2, the InternalRel of R2] and
A5: z = R2 ; ::_thesis: y = z
 the carrier of R1 = the carrier of R2 by A2, A4, XTUPLE_0:1;
hence  y = z by A2, A3, A4, A5, XTUPLE_0:1; ::_thesis: verum
end;
consider X being set  such that
A6: for x being set holds
( x in X iff ex y being set st
( y in FinSETS & S1[y,x] ) ) from TARSKI:sch_1(A1);
take  X ; ::_thesis: for X being set holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
 for x being set holds
( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
proof
let x be set ; ::_thesis: ( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
thus  ( x in X implies ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) ) ::_thesis: ( ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) implies x in X )
proof
assume  x in X ; ::_thesis: ex R being strict RelStr st
( x = R & the carrier of R in FinSETS )
then consider y being set  such that
A7: y in FinSETS and
A8: ex R being strict RelStr st
( y = [ the carrier of R, the InternalRel of R] & x = R ) by A6;
consider R being strict RelStr  such that
A9: y = [ the carrier of R, the InternalRel of R] and
A10: x = R by A8;
A11: { the carrier of R} in {{ the carrier of R, the InternalRel of R},{ the carrier of R}} by TARSKI:def_2;
 {{ the carrier of R, the InternalRel of R},{ the carrier of R}} c= FinSETS by A7, A9, ORDINAL1:def_2;
then A12: { the carrier of R} c= FinSETS by A11, ORDINAL1:def_2;
 the carrier of R in { the carrier of R} by TARSKI:def_1;
hence  ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) by A10, A12; ::_thesis: verum
end;
given R being strict RelStr  such that A13: x = R and
A14: the carrier of R in FinSETS ; ::_thesis: x in X
consider R being strict RelStr  such that
A15: x = R and
A16: the carrier of R in FinSETS by A13, A14;
 the InternalRel of R in FinSETS by A16, Th1;
then  [ the carrier of R, the InternalRel of R] in FinSETS by A16, CLASSES2:58;
hence  x in X by A6, A15; ::_thesis: verum
end;
hence  for X being set holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) & ( for X being set holds
( X in b2 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex R being strict RelStr st
( $1 = R & the carrier of R in FinSETS );
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def_4_:_
 for b1 being set holds
( b1 = fin_RelStr iff for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) );

registration
cluster fin_RelStr  ->  non empty ;
correctness
coherence
not fin_RelStr is empty ;
proof
 RelStr(# {},({} ({},{})) #) in fin_RelStr
proof
set X = RelStr(# {},({} ({},{})) #);
 the carrier of RelStr(# {},({} ({},{})) #) in FinSETS by CLASSES1:2, CLASSES2:def_2;
hence  RelStr(# {},({} ({},{})) #) in fin_RelStr by Def4; ::_thesis: verum
end;
hence  not fin_RelStr is empty ; ::_thesis: verum
end;
end;

definition
func fin_RelStr_sp  ->  Subset of fin_RelStr means :Def5: :: NECKLA_2:def 5
( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in it ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in it & H2 in it holds
( union_of (H1,H2) in it & sum_of (H1,H2) in it ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
it c= M ) );
existence
 ex b1 being Subset of fin_RelStr st
( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b1 c= M ) )
proof
defpred S1[ set ] means ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in $1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in $1 & H2 in $1 holds
( union_of (H1,H2) in $1 & sum_of (H1,H2) in $1 ) ) );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool fin_RelStr & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in X holds
x in bool fin_RelStr by A1;
then reconsider X = X as Subset-Family of fin_RelStr by TARSKI:def_3;
take IT = Intersect X; ::_thesis: ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in IT ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of (H1,H2) in IT & sum_of (H1,H2) in IT ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
IT c= M ) )
A2: S1[ fin_RelStr ]
proof
set A = fin_RelStr ;
 for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr & H2 in fin_RelStr holds
( union_of (H1,H2) in fin_RelStr & sum_of (H1,H2) in fin_RelStr )
proof
let H1, H2 be strict RelStr ; ::_thesis: ( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr & H2 in fin_RelStr implies ( union_of (H1,H2) in fin_RelStr & sum_of (H1,H2) in fin_RelStr ) )
assume that
 the carrier of H1 misses the carrier of H2 and
A3: H1 in fin_RelStr and
A4: H2 in fin_RelStr ; ::_thesis: ( union_of (H1,H2) in fin_RelStr & sum_of (H1,H2) in fin_RelStr )
consider S2 being strict RelStr  such that
A5: S2 = H2 and
A6: the carrier of S2 in FinSETS by A4, Def4;
reconsider RS9 = sum_of (H1,H2) as strict RelStr ;
consider S1 being strict RelStr  such that
A7: S1 = H1 and
A8: the carrier of S1 in FinSETS by A3, Def4;
reconsider RS = union_of (S1,S2) as strict RelStr ;
A9: the carrier of H1 \/ the carrier of H2 in FinSETS by A7, A8, A5, A6, CLASSES2:60;
then  the carrier of RS in FinSETS by A7, A5, Def2;
hence  union_of (H1,H2) in fin_RelStr by A7, A5, Def4; ::_thesis: sum_of (H1,H2) in fin_RelStr
 the carrier of RS9 in FinSETS by A9, Def3;
hence  sum_of (H1,H2) in fin_RelStr by Def4; ::_thesis: verum
end;
hence  S1[ fin_RelStr ] by Def4; ::_thesis: verum
end;
 fin_RelStr in bool fin_RelStr by ZFMISC_1:def_1;
then A10: X <> {} by A1, A2;
then A11: IT = meet X by SETFAM_1:def_9;
 ( S1[IT] & ( for X being Subset of fin_RelStr st S1[X] holds
IT c= X ) )
proof
A12: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of (H1,H2) in IT & sum_of (H1,H2) in IT )
proof
let H1, H2 be strict RelStr ; ::_thesis: ( the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT implies ( union_of (H1,H2) in IT & sum_of (H1,H2) in IT ) )
assume that
A13: the carrier of H1 misses the carrier of H2 and
A14: H1 in IT and
A15: H2 in IT ; ::_thesis: ( union_of (H1,H2) in IT & sum_of (H1,H2) in IT )
A16: for Y being set st Y in X holds
sum_of (H1,H2) in Y
proof
let Y be set ; ::_thesis: ( Y in X implies sum_of (H1,H2) in Y )
assume A17: Y in X ; ::_thesis: sum_of (H1,H2) in Y
then A18: H2 in Y by A11, A15, SETFAM_1:def_1;
 H1 in Y by A11, A14, A17, SETFAM_1:def_1;
hence  sum_of (H1,H2) in Y by A1, A13, A17, A18; ::_thesis: verum
end;
 for Y being set st Y in X holds
union_of (H1,H2) in Y
proof
let Y be set ; ::_thesis: ( Y in X implies union_of (H1,H2) in Y )
assume A19: Y in X ; ::_thesis: union_of (H1,H2) in Y
then A20: H2 in Y by A11, A15, SETFAM_1:def_1;
 H1 in Y by A11, A14, A19, SETFAM_1:def_1;
hence  union_of (H1,H2) in Y by A1, A13, A19, A20; ::_thesis: verum
end;
hence  ( union_of (H1,H2) in IT & sum_of (H1,H2) in IT ) by A10, A11, A16, SETFAM_1:def_1; ::_thesis: verum
end;
 for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in IT
proof
let R be strict RelStr ; ::_thesis: ( the carrier of R is 1 -element & the carrier of R in FinSETS implies R in IT )
assume that
A21: the carrier of R is 1 -element and
A22: the carrier of R in FinSETS ; ::_thesis: R in IT
 for Y being set st Y in X holds
R in Y by A1, A21, A22;
hence  R in IT by A10, A11, SETFAM_1:def_1; ::_thesis: verum
end;
hence  S1[IT] by A12; ::_thesis: for X being Subset of fin_RelStr st S1[X] holds
IT c= X
let Y be Subset of fin_RelStr; ::_thesis: ( S1[Y] implies IT c= Y )
assume A23: S1[Y] ; ::_thesis: IT c= Y
 IT c= Y
proof
A24: Y in X by A1, A23;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in IT or x in Y )
assume  x in IT ; ::_thesis: x in Y
hence  x in Y by A11, A24, SETFAM_1:def_1; ::_thesis: verum
end;
hence  IT c= Y ; ::_thesis: verum
end;
hence  ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in IT ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of (H1,H2) in IT & sum_of (H1,H2) in IT ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
IT c= M ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b1 c= M ) & ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b2 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b2 & H2 in b2 holds
( union_of (H1,H2) in b2 & sum_of (H1,H2) in b2 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b2 c= M ) holds
b1 = b2
proof
let X1, X2 be Subset of fin_RelStr; ::_thesis: ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in X1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X1 & H2 in X1 holds
( union_of (H1,H2) in X1 & sum_of (H1,H2) in X1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
X1 c= M ) & ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in X2 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X2 & H2 in X2 holds
( union_of (H1,H2) in X2 & sum_of (H1,H2) in X2 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
X2 c= M ) implies X1 = X2 )
assume that
A25: for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in X1 and
A26: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X1 & H2 in X1 holds
( union_of (H1,H2) in X1 & sum_of (H1,H2) in X1 ) and
A27: for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
X1 c= M and
A28: for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in X2 and
A29: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X2 & H2 in X2 holds
( union_of (H1,H2) in X2 & sum_of (H1,H2) in X2 ) and
A30: for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
X2 c= M ; ::_thesis: X1 = X2
A31: X2 c= X1 by A25, A26, A30;
 X1 c= X2 by A27, A28, A29;
hence  X1 = X2 by A31, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines fin_RelStr_sp NECKLA_2:def_5_:_
 for b1 being Subset of fin_RelStr holds
( b1 = fin_RelStr_sp iff ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b1 c= M ) ) );

registration
cluster fin_RelStr_sp  ->  non empty ;
correctness
coherence
not fin_RelStr_sp is empty ;
proof
 [:{0},{0}:] c= [:{0},{0}:] ;
then reconsider R = [:{0},{0}:] as Relation of {0} ;
 RelStr(# {0},R #) in fin_RelStr_sp
proof
set X = RelStr(# {0},R #);
A1: the carrier of RelStr(# {0},R #) in FinSETS by CLASSES2:56, CLASSES2:57;
thus  RelStr(# {0},R #) in fin_RelStr_sp by A1, Def5; ::_thesis: verum
end;
hence  not fin_RelStr_sp is empty ; ::_thesis: verum
end;
end;

theorem Th4: :: NECKLA_2:4
for X being set st X in fin_RelStr_sp holds
X is non empty finite strict RelStr
proof
let X be set ; ::_thesis: ( X in fin_RelStr_sp implies X is non empty finite strict RelStr )
assume A1: X in fin_RelStr_sp ; ::_thesis: X is non empty finite strict RelStr
then A2: ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) by Def4;
then reconsider R = X as strict RelStr ;
now__::_thesis:_not_R_is_empty
set M = fin_RelStr_sp \ {R};
set F = fin_RelStr_sp ;
reconsider M = fin_RelStr_sp \ {R} as Subset of fin_RelStr ;
A3: R in {R} by TARSKI:def_1;
assume A4: R is empty ; ::_thesis: contradiction
A5: now__::_thesis:_for_H1,_H2_being_strict_RelStr_st_the_carrier_of_H1_misses_the_carrier_of_H2_&_H1_in_M_&_H2_in_M_holds_
(_union_of_(H1,H2)_in_M_&_sum_of_(H1,H2)_in_M_)
let H1, H2 be strict RelStr ; ::_thesis: ( the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M implies ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) )
assume that
A6: the carrier of H1 misses the carrier of H2 and
A7: H1 in M and
A8: H2 in M ; ::_thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )
A9: H2 in fin_RelStr_sp by A8, XBOOLE_0:def_5;
A10: not H1 in {R} by A7, XBOOLE_0:def_5;
 the carrier of H1 <> {}
proof
percases ( the carrier of H1 <> the carrier of R or the InternalRel of H1 <> the InternalRel of R ) by A10, TARSKI:def_1;
suppose the carrier of H1 <> the carrier of R ; ::_thesis: the carrier of H1 <> {}
hence  the carrier of H1 <> {} by A4; ::_thesis: verum
end;
supposeA11: the InternalRel of H1 <> the InternalRel of R ; ::_thesis: the carrier of H1 <> {}
set InterH1 = the InternalRel of H1;
 the InternalRel of H1 <> {} by A4, A11;
hence  the carrier of H1 <> {} ; ::_thesis: verum
end;
end;
end;
then reconsider A = the carrier of H1 as non empty set ;
 A \/ the carrier of H2 <> {} ;
then  union_of (H1,H2) <> R by A4, Def2;
then A12: not union_of (H1,H2) in {R} by TARSKI:def_1;
 the carrier of (sum_of (H1,H2)) = A \/ the carrier of H2 by Def3;
then A13: not sum_of (H1,H2) in {R} by A4, TARSKI:def_1;
A14: H1 in fin_RelStr_sp by A7, XBOOLE_0:def_5;
then  union_of (H1,H2) in fin_RelStr_sp by A6, A9, Def5;
hence  union_of (H1,H2) in M by A12, XBOOLE_0:def_5; ::_thesis: sum_of (H1,H2) in M
 sum_of (H1,H2) in fin_RelStr_sp by A6, A14, A9, Def5;
hence  sum_of (H1,H2) in M by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_S_being_strict_RelStr_st_the_carrier_of_S_is_1_-element_&_the_carrier_of_S_in_FinSETS_holds_
S_in_M
let S be strict RelStr ; ::_thesis: ( the carrier of S is 1 -element & the carrier of S in FinSETS implies S in M )
assume that
A15: the carrier of S is 1 -element and
A16: the carrier of S in FinSETS ; ::_thesis: S in M
A17: not S in {R} by A4, A15, TARSKI:def_1;
 S in fin_RelStr_sp by A15, A16, Def5;
hence  S in M by A17, XBOOLE_0:def_5; ::_thesis: verum
end;
then  fin_RelStr_sp c= M by A5, Def5;
hence  contradiction by A1, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  X is non empty finite strict RelStr by A2; ::_thesis: verum
end;

theorem :: NECKLA_2:5
for R being RelStr st R in fin_RelStr_sp holds
the carrier of R in FinSETS
proof
let R be RelStr ; ::_thesis: ( R in fin_RelStr_sp implies the carrier of R in FinSETS )
assume  R in fin_RelStr_sp ; ::_thesis: the carrier of R in FinSETS
then  ex S being strict RelStr st
( R = S & the carrier of S in FinSETS ) by Def4;
hence  the carrier of R in FinSETS ; ::_thesis: verum
end;

theorem Th6: :: NECKLA_2:6
for X being set holds
( not X in fin_RelStr_sp or X 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )
proof
deffunc H1( set , set ) ->  set = $2 \/  {  x where x is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in $2 & R2 in $2 & ( x = union_of (R1,R2) or x = sum_of (R1,R2) ) )  }  ;
set Y = fin_RelStr_sp ;
let X be set ; ::_thesis: ( not X in fin_RelStr_sp or X 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )
assume A1: X in fin_RelStr_sp ; ::_thesis: ( X 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )
consider f being Function such that
A2: dom f = NAT and
A3: f . 0 =  {  x where x is Element of fin_RelStr_sp : x is trivial RelStr  }  and
A4: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_11();
A5: Union f c= fin_RelStr_sp
proof
defpred S1[ Nat] means f . $1 c= fin_RelStr_sp ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Union f or y in fin_RelStr_sp )
assume  y in Union f ; ::_thesis: y in fin_RelStr_sp
then consider x being set  such that
A6: x in dom f and
A7: y in f . x by CARD_5:2;
reconsider x = x as Element of NAT by A2, A6;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
A10:  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  c= fin_RelStr_sp
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  or x in fin_RelStr_sp )
set S =  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ;
assume  x in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ; ::_thesis: x in fin_RelStr_sp
then  ex a being Element of fin_RelStr_sp st
( x = a & ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;
hence  x in fin_RelStr_sp ; ::_thesis: verum
end;
 f . (k + 1) = (f . k) \/  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  by A4;
hence  S1[k + 1] by A9, A10, XBOOLE_1:8; ::_thesis: verum
end;
A11: S1[ 0 ]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f . 0 or y in fin_RelStr_sp )
assume  y in f . 0 ; ::_thesis: y in fin_RelStr_sp
then  ex a being Element of fin_RelStr_sp st
( y = a & a is trivial RelStr ) by A3;
hence  y in fin_RelStr_sp ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A11, A8);
then  f . x c= fin_RelStr_sp ;
hence  y in fin_RelStr_sp by A7; ::_thesis: verum
end;
then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A12: for i being Nat holds f . i c= f . (i + 1)
proof
let i be Nat; ::_thesis: f . i c= f . (i + 1)
A13: f . (i + 1) = (f . i) \/  {  b where b is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . i & R2 in f . i & ( b = union_of (R1,R2) or b = sum_of (R1,R2) ) )  }  by A4;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f . i or x in f . (i + 1) )
assume  x in f . i ; ::_thesis: x in f . (i + 1)
hence  x in f . (i + 1) by A13, XBOOLE_0:def_3; ::_thesis: verum
end;
A14: for i, j being Element of NAT st i <= j holds
f . i c= f . j
proof
let i, j be Element of NAT ; ::_thesis: ( i <= j implies f . i c= f . j )
defpred S1[ Nat] means f . i c= f . (i + $1);
assume  i <= j ; ::_thesis: f . i c= f . j
then A15: ex k being Nat st j = i + k by NAT_1:10;
A16: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A17: S1[k] ; ::_thesis: S1[k + 1]
 f . (i + k) c= f . ((i + k) + 1) by A12;
hence  S1[k + 1] by A17, XBOOLE_1:1; ::_thesis: verum
end;
A18: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A18, A16);
hence  f . i c= f . j by A15; ::_thesis: verum
end;
A19: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M )
proof
let H1, H2 be strict RelStr ; ::_thesis: ( the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M implies ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) )
assume that
A20: the carrier of H1 misses the carrier of H2 and
A21: H1 in M and
A22: H2 in M ; ::_thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )
consider x2 being set  such that
A23: x2 in dom f and
A24: H2 in f . x2 by A22, CARD_5:2;
consider x1 being set  such that
A25: x1 in dom f and
A26: H1 in f . x1 by A21, CARD_5:2;
reconsider x1 = x1, x2 = x2 as Element of NAT by A2, A25, A23;
set W =  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ;
A27: f . ((max (x1,x2)) + 1) = (f . (max (x1,x2))) \/  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  by A4;
A29: f . x1 c= f . (max (x1,x2)) by A14, XXREAL_0:25;
A30: f . x2 c= f . (max (x1,x2)) by A14, XXREAL_0:25;
 sum_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;
then  sum_of (H1,H2) in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  by A20, A26, A24, A29, A30;
then A31: sum_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def_3;
 union_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;
then  union_of (H1,H2) in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  by A20, A26, A24, A29, A30;
then  union_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def_3;
hence  ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) by A2, A31, CARD_5:2; ::_thesis: verum
end;
 for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M
proof
A32: f . 0 c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f . 0 or x in M )
assume  x in f . 0 ; ::_thesis: x in M
hence  x in M by A2, CARD_5:2; ::_thesis: verum
end;
let R be strict RelStr ; ::_thesis: ( the carrier of R is 1 -element & the carrier of R in FinSETS implies R in M )
assume that
A33: the carrier of R is 1 -element and
A34: the carrier of R in FinSETS ; ::_thesis: R in M
A35: R is trivial RelStr by A33;
 R is Element of fin_RelStr_sp by A33, A34, Def5;
then  R in f . 0 by A3, A35;
hence  R in M by A32; ::_thesis: verum
end;
then A36: fin_RelStr_sp c= M by A19, Def5;
then A37: Union f = fin_RelStr_sp by A5, XBOOLE_0:def_10;
assume A38: X is not 1 -element strict RelStr ; ::_thesis: 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
proof
defpred S1[ Nat] means ( X in f . $1 implies 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) );
A39: for k being Nat st S1[k] holds
S1[k + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A40: S1[n] ; ::_thesis: S1[n + 1]
set W =  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ;
assume A41: X in f . (n + 1) ; ::_thesis: 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A42: f . (n + 1) = (f . n) \/  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  by A4;
percases ( X in f . n or X in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ) by A41, A42, XBOOLE_0:def_3;
suppose X in f . n ; ::_thesis: 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
hence  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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A40; ::_thesis: verum
end;
suppose X in  {  a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) )  }  ; ::_thesis: 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
then  ex a being Element of fin_RelStr_sp st
( a = X & ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;
then consider R1, R2 being strict RelStr  such that
A43: the carrier of R1 misses the carrier of R2 and
A44: R1 in f . n and
A45: R2 in f . n and
A46: ( X = union_of (R1,R2) or X = sum_of (R1,R2) ) ;
A47: R2 in fin_RelStr_sp by A2, A37, A45, CARD_5:2;
 R1 in fin_RelStr_sp by A2, A37, A44, CARD_5:2;
hence  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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A43, A46, A47; ::_thesis: verum
end;
end;
end;
A48: S1[ 0 ]
proof
assume  X in f . 0 ; ::_thesis: 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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )
then consider a being Element of fin_RelStr_sp  such that
A49: ( X = a & a is trivial RelStr ) by A3;
 a is non empty strict RelStr by Th4;
then  a is non empty trivial strict RelStr by A49;
then reconsider a = a as non empty trivial strict RelStr ;
 a is 1 -element strict RelStr ;
hence  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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A38, A49; ::_thesis: verum
end;
A50: for n being Nat holds S1[n] from NAT_1:sch_2(A48, A39);
 ex y being set st
( y in dom f & X in f . y ) by A1, A36, CARD_5:2;
hence  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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A2, A50; ::_thesis: verum
end;
hence  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 & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) ; ::_thesis: verum
end;

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

theorem :: NECKLA_2:7
for R being non empty strict RelStr st R in fin_RelStr_sp holds
R is N-free
proof
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;
percases ( 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;
supposeA7: 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 (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 & 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 (Necklace 4)
proof
assume A22: [1,3] in the InternalRel of (Necklace 4) ; ::_thesis: contradiction
percases ( [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;
suppose [1,3] = [0,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [1,3] = [1,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [1,3] = [2,3] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [1,3] = [3,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [1,3] = [2,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [1,3] = [1,0] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
A23: not [0,2] in the InternalRel of (Necklace 4)
proof
assume A24: [0,2] in the InternalRel of (Necklace 4) ; ::_thesis: contradiction
percases ( [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;
suppose [0,2] = [0,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,2] = [1,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,2] = [2,3] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,2] = [3,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,2] = [2,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,2] = [1,0] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
A25: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;
then A26: 0 in the carrier of (Necklace 4) by ENUMSET1:def_2;
A27: not [0,3] in the InternalRel of (Necklace 4)
proof
assume A28: [0,3] in the InternalRel of (Necklace 4) ; ::_thesis: contradiction
percases ( [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;
suppose [0,3] = [0,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,3] = [1,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,3] = [2,3] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,3] = [3,2] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,3] = [2,1] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
suppose [0,3] = [1,0] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
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 set ; :: 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;
A33: rng the InternalRel of S c= the carrier of S by RELAT_1:def_19;
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
let x be set ; :: 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;
A37: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def_19;
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;
percases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by A49, XBOOLE_0:def_3;
supposeA55: 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 A55, ZFMISC_1:87;
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 A55, ZFMISC_1:87;
hence  contradiction by A40, A26, A34, A27, A31; ::_thesis: verum
end;
then A62: f . 3 in the carrier of H1 by A47, XBOOLE_0:def_3;
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 A62, ZFMISC_1:87;
hence  contradiction by A40, A38, A34, A21, A35; ::_thesis: verum
end;
A64: dom f = the carrier of (Necklace 4) by FUNCT_2:def_1;
 rng f c= the carrier of H1
proof
let y be set ; :: 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 set  such that
A65: x in dom f and
A66: y = f . x by FUNCT_1:def_3;
percases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A64, A65, Lm1, ENUMSET1:def_2;
suppose x = 0 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A55, A66; ::_thesis: verum
end;
suppose x = 1 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A50, A63, A66, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A53, A57, A66, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 3 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A47, A61, A66, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A67: f is Function of the carrier of (Necklace 4), the carrier of H1 by FUNCT_2:6;
 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;
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 A30, A41, Def3;
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
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 A30, A52, Def3;
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
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 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 ;
A77: not H2 is empty by A18, Th4;
A78: cH1 <> cS
proof
A79: cS = cH1 \/ cH2 by A30, Def3;
assume A80: cH1 = cS ; ::_thesis: contradiction
consider x being set  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;
 cS = cH1 \/ cH2 by A30, Def3;
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
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) )
proof
assume A85: [x,y] in the InternalRel of (Necklace 4) ; ::_thesis: [(f . x),(f . y)] in the InternalRel of H1
percases ( [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;
supposeA86: [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;
supposeA87: [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;
supposeA88: [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;
supposeA89: [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;
supposeA90: [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;
supposeA91: [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;
end;
end;
thus  ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) ) ::_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;
end;
then  H1 embeds Necklace 4 by A39, A67, NECKLACE:def_1;
hence  ex n being Nat st
( n < m & S1[n] ) by A5, A17, A68, A82; ::_thesis: verum
end;
supposeA93: 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 A93, ZFMISC_1:87;
hence  contradiction by A40, A26, A34, A27, A35; ::_thesis: verum
end;
then A97: f . 3 in the carrier of H2 by A47, XBOOLE_0:def_3;
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;
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 A30, A41, Def3;
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;
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 A93, ZFMISC_1:87;
hence  contradiction by A40, A26, A42, A23, A35; ::_thesis: verum
end;
A103: dom f = the carrier of (Necklace 4) by FUNCT_2:def_1;
 rng f c= the carrier of H2
proof
let y be set ; :: 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 set  such that
A104: x in dom f and
A105: y = f . x by FUNCT_1:def_3;
percases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A103, A104, Lm1, ENUMSET1:def_2;
suppose x = 0 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A93, A105; ::_thesis: verum
end;
suppose x = 1 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A50, A98, A105, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A53, A102, A105, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 3 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A47, A96, A105, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A106: f is Function of the carrier of (Necklace 4), the carrier of H2 by FUNCT_2:6;
 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;
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 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 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
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 A30, A52, Def3;
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
A118: cS = cH1 \/ cH2 by A30, Def3;
assume A119: cH2 = cS ; ::_thesis: contradiction
consider x being set  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;
 cS = cH1 \/ cH2 by A30, Def3;
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
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) )
proof
assume A123: [x,y] in the InternalRel of (Necklace 4) ; ::_thesis: [(f . x),(f . y)] in the InternalRel of H2
percases ( [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;
supposeA124: [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;
supposeA125: [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;
supposeA126: [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;
supposeA127: [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;
supposeA128: [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;
supposeA129: [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;
end;
end;
thus  ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) ::_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;
end;
then  H2 embeds Necklace 4 by A39, A106, NECKLACE:def_1;
hence  ex n being Nat st
( n < m & S1[n] ) by A5, A18, A107, A121; ::_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 (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 & S1[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;
percases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by A140, XBOOLE_0:def_3;
supposeA147: 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 (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
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 A138, A146, Def2;
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
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 A18, Th4;
A161: cH1 <> cS
proof
A162: cS = cH1 \/ cH2 by A138, Def2;
assume A163: cH1 = cS ; ::_thesis: contradiction
consider x being set  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;
 cS = cH1 \/ cH2 by A138, Def2;
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
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 A167, XBOOLE_0:def_3;
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 A166, XBOOLE_0:def_3;
 [(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
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 A138, A142, Def2;
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
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) )
proof
assume A175: [x,y] in the InternalRel of (Necklace 4) ; ::_thesis: [(f . x),(f . y)] in the InternalRel of H1
percases ( [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;
supposeA176: [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;
supposeA177: [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;
supposeA178: [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;
supposeA179: [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;
supposeA180: [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;
supposeA181: [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;
end;
end;
thus  ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) ) ::_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;
end;
A183: f . 3 in rng the InternalRel of H1 by A170, XTUPLE_0:def_13;
 rng f c= the carrier of H1
proof
let y be set ; :: 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 set  such that
A184: x in dom f and
A185: y = f . x by FUNCT_1:def_3;
percases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A148, A184, Lm1, ENUMSET1:def_2;
suppose x = 0 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A147, A185; ::_thesis: verum
end;
suppose x = 1 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A156, A158, A185; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A156, A169, A185; ::_thesis: verum
end;
suppose x = 3 ; ::_thesis: y in the carrier of H1
hence  y in the carrier of H1 by A156, A183, A185; ::_thesis: verum
end;
end;
end;
then  f is Function of the carrier of (Necklace 4), the carrier of H1 by FUNCT_2:6;
then  H1 embeds Necklace 4 by A136, A174, NECKLACE:def_1;
hence  ex n being Nat st
( n < m & S1[n] ) by A5, A17, A155, A165; ::_thesis: verum
end;
supposeA186: 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 (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
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 A138, A146, Def2;
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
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 A17, Th4;
A200: cH2 <> cS
proof
A201: cS = cH1 \/ cH2 by A138, Def2;
assume A202: cH2 = cS ; ::_thesis: contradiction
consider x being set  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;
 cS = cH1 \/ cH2 by A138, Def2;
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
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 A206, XBOOLE_0:def_3;
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 A205, XBOOLE_0:def_3;
 [(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
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 A138, A142, Def2;
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
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) )
proof
assume A214: [x,y] in the InternalRel of (Necklace 4) ; ::_thesis: [(f . x),(f . y)] in the InternalRel of H2
percases ( [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;
supposeA215: [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;
supposeA216: [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;
supposeA217: [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;
supposeA218: [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;
supposeA219: [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;
supposeA220: [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;
end;
end;
thus  ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) ::_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;
end;
A222: f . 3 in rng the InternalRel of H2 by A209, XTUPLE_0:def_13;
 rng f c= the carrier of H2
proof
let y be set ; :: 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 set  such that
A223: x in dom f and
A224: y = f . x by FUNCT_1:def_3;
percases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A187, A223, Lm1, ENUMSET1:def_2;
suppose x = 0 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A186, A224; ::_thesis: verum
end;
suppose x = 1 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A195, A197, A224; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A195, A208, A224; ::_thesis: verum
end;
suppose x = 3 ; ::_thesis: y in the carrier of H2
hence  y in the carrier of H2 by A195, A222, A224; ::_thesis: verum
end;
end;
end;
then  f is Function of the carrier of (Necklace 4), the carrier of H2 by FUNCT_2:6;
then  H2 embeds Necklace 4 by A136, A213, NECKLACE:def_1;
hence  ex n being Nat st
( n < m & S1[n] ) by A5, A18, A194, A204; ::_thesis: verum
end;
end;
end;
hence  ex n being Nat st
( n < m & S1[n] ) by A19, A20; ::_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 NAT_1:sch_7(A225, A2);
hence  contradiction ; ::_thesis: verum
end;