:: deftheorem defines empty-yielding PRE_POLY:def 18 :
for X being set
for b being bag of X holds
( b is empty-yielding iff b = EmptyBag X );