theorem :: NECKLA_2:7

for R being non empty strict RelStr st R in fin_RelStr_sp holds
R is N-free