theorem :: PBOOLE:122

for X being ManySortedSet of {} holds X = {} ;