theorem :: MMLQUERY:79

for X being ConstructorDB
for A being FinSequence of the Constrs of X
for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)