theorem Th59: :: PBOOLE:59

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