theorem Th132: :: PBOOLE:132

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