:: deftheorem Def4 defines fin_RelStr NECKLA_2:def 4 :
for b₁ being set holds
( b₁ = fin_RelStr iff for X being object holds
( X in b₁ iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) );