theorem :: PBOOLE:134

for I being set
for X being non-empty ManySortedSet of I ex x being ManySortedSet of I st x in X