let R be non empty RelStr ; :: thesis: ( R is trivial & R is strict implies R is N-free )
set Y = Necklace 4;
assume ( R is trivial & R is strict ) ; :: thesis: R is N-free
then consider y being set 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 one-to-one & ( 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 NECKLACE:def 2;
A3: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1
.= {0 ,1,2,3} by NECKLACE:2, NECKLACE:21 ;
then A4: 0 in dom f by ENUMSET1:def 2;
A5: 1 in dom f by A3, ENUMSET1:def 2;
A6: f . 0 in {y} by A1, A4, PARTFUN1:27;
f . 1 in {y} by A1, A5, PARTFUN1:27;
then ( f . 0 = y & f . 1 = y ) by A6, TARSKI:def 1;
hence contradiction by A2, A4, A5, FUNCT_1:def 8; :: thesis: verum