for b being bag of {} holds b = EmptyBag {}