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