theorem :: PBOOLE:129

for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff X = EmptyMS I )