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