theorem Th124: :: PBOOLE:124

for I being non empty set
for x being ManySortedSet of I holds not x in EmptyMS I