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