theorem Th71: :: MMLQUERY:71

for n, m being Nat
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y st n <= m holds
ATMOST+ (B,n) c= ATMOST+ (B,m)