theorem Th33: :: MONOID_1:33

for A being non empty set
for a being Element of A holds chi a is Element of (finite-MultiSet_over A)