set Y = Necklace 4;

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

assume ( R is trivial & R is strict ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

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

assume ( R is trivial & R is strict ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum