for S being set
for X being ManySortedSet of S
for Y being V5() ManySortedSet of S
for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y