theorem :: PBOOLE:57

for I being set
for X, Y being ManySortedSet of I st X c= Y (\) X holds
X = EmptyMS I