theorem :: PBOOLE:130

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