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