reconsider I = {} as Relation of n,n by RELSET_1:25;
set R = RelStr(# n,I #);
reconsider R = RelStr(# n,I #) as NatRelStr of n by LNRS;
R is irreflexive

proof

let x be set ; :: according to NECKLACE:def 6 :: thesis: ( not x in the carrier of R or not [x,x] in the InternalRel of R )
assume x in the carrier of R ; :: thesis: not [x,x] in the InternalRel of R
thus not [x,x] in the InternalRel of R ; :: thesis: verum

end;

hence ex b₁ being NatRelStr of n st b₁ is irreflexive ; :: thesis: verum