:: deftheorem defines occur MMLQUERY:def 29 :
for X being ConstructorDB
for a being Element of X holds a occur = a . ((@ the ref-operation of X) ~);