set Y = Necklace 4;
let R be non empty RelStr ; ( R is trivial & R is strict implies R is N-free )
assume
( R is trivial & R is strict )
; R is N-free
then consider y being object such that
A1:
the carrier of R = {y}
by GROUP_6:def 2;
assume
not R is N-free
; contradiction
then
R embeds Necklace 4
by NECKLA_2:def 1;
then consider f being Function of (Necklace 4),R such that
A2:
f is V24()
and
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 )
;
A3: dom f =
the carrier of (Necklace 4)
by FUNCT_2:def 1
.=
{0,1,2,3}
by NECKLACE:1, NECKLACE:20
;
then A4:
1 in dom f
by ENUMSET1:def 2;
then
f . 1 in {y}
by A1, PARTFUN1:4;
then A5:
f . 1 = y
by TARSKI:def 1;
A6:
0 in dom f
by A3, ENUMSET1:def 2;
then
f . 0 in {y}
by A1, PARTFUN1:4;
then
f . 0 = y
by TARSKI:def 1;
hence
contradiction
by A2, A6, A4, A5, FUNCT_1:def 4; verum