:: deftheorem Def35 defines ATMOST+ MMLQUERY:def 35 :
for X being ref-finite ConstructorDB
for A being FinSequence of the Constrs of X
for n being Nat st the carrier of X <> {} holds
ATMOST+ (A,n) = { x where x is Element of X : card ((x ref) \ (rng A)) <= n } ;