:: deftheorem Def6 defines finite-membered FINSET_1:def 6 :
for A being set holds
( A is finite-membered iff for B being set st B in A holds
B is finite );