:: deftheorem Def30 defines ref-finite MMLQUERY:def 30 :
for X being ConstructorDB holds
( X is ref-finite iff for x being Element of X holds x ref is finite );