for X being Ordinal
for a, b being finite Subset of X st a <> b holds
(a,1) -bag <> (b,1) -bag