theorem :: PBOOLE:129

for I being set
for X being ManySortedSet of I holds
( X is V9() iff X = EmptyMS I )