:: deftheorem Def32 defines ATMOST MMLQUERY:def 32 :
for X being ConstructorDB
for A being FinSequence of the Constrs of X st the carrier of X <> {} holds
ATMOST A = { x where x is Element of X : x ref c= rng A } ;