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 )

hence ( R is strict & R is finite & R is N-free ) ; :: thesis: verum

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

then
not R embeds Necklace 4
by NECKLACE:def 1;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;( ( [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

hence ( R is strict & R is finite & R is N-free ) ; :: thesis: verum