theorem Th6: :: LEXBFS:6

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