theorem Th131: :: PBOOLE:131

for I being set
for X, Y being ManySortedSet of I st X is non-empty & X c= Y holds
Y is non-empty