theorem Th44: :: PBOOLE:44

for I being set
for X being ManySortedSet of I st X c= EmptyMS I holds
X = EmptyMS I