theorem :: VALUED_0:32

for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M by Lm1;