theorem Th2: :: PRE_CIRC:3

for I being non empty set
for B being non-empty ManySortedSet of I holds not union (rng B) is empty