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 (),R st f is one-to-one holds
ex x, y being Element of () st
( ( [x,y] in the InternalRel of () 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 () ) )
let f be Function of (),R; :: thesis: ( f is one-to-one implies ex x, y being Element of () st
( ( [x,y] in the InternalRel of () 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 () ) ) )

A1: dom f = the carrier of () by FUNCT_2:def 1
.= {0,1,2,3} by ;
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 ;
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 ;
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 () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of R )

then A9: f . 2 <> f . 3 by ;
f . 1 <> f . 3 by ;
hence not for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of R ) by ; :: thesis: verum
end;
then not R embeds Necklace 4 by NECKLACE:def 1;
hence ( R is strict & R is finite & R is N-free ) ; :: thesis: verum