theorem :: PBOOLE:134

for I being set
for X being V8() ManySortedSet of I ex x being ManySortedSet of I st x in X