for X being non empty set
for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds
x1 = x2