:: deftheorem defines UnitBag HILBASIS:def 2 :
for X being set
for x being Element of X holds UnitBag x = (EmptyBag X) +* (x,1);