theorem Th6: :: PBOOLE:6

for I being set
for X being ManySortedSet of I st ( for i being object st i in I holds
X . i = {} ) holds
X = EmptyMS I