:: deftheorem defines empty-yielding PBOOLE:def 12 :
for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff for i being object st i in I holds
X . i is empty );