theorem :: PBOOLE:84

for I being set
for X being ManySortedSet of I holds X (\+\) (EmptyMS I) = X