theorem :: PBOOLE:130

for I being set
for X, Y being ManySortedSet of I st Y is V9() & X c= Y holds
X is V9()