for X being set
for b being bag of X holds b / b = EmptyBag X