theorem :: PBOOLE:137

for I being set
for M being non-empty ManySortedSet of I holds not {} in rng M