:: deftheorem defines N-free NECKLA_2:def 1 :
for G being non empty RelStr holds
( G is N-free iff not G embeds Necklace 4 );