for I being set
for a, b being bag of I st a <> EmptyBag I holds
a + b <> EmptyBag I