theorem Th54: :: MMLQUERY:54

for A being FinSequence
for a being set holds #occurrences (a,A) <= len A