theorem :: NECKLA_3:40

for G being non empty finite strict symmetric irreflexive RelStr st G is N-free & the carrier of G in FinSETS holds
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp