let X be Ordinal; :: thesis: for a, b being finite Subset of X st a <> b holds
a,1 -bag <> b,1 -bag
let a, b be finite Subset of X; :: thesis: ( a <> b implies a,1 -bag <> b,1 -bag )
assume A1: a <> b ; :: thesis: a,1 -bag <> b,1 -bag
assume A2: a,1 -bag = b,1 -bag ; :: thesis: contradiction

now

let x be set ; :: thesis: ( x in a iff x in b )
( x in a iff (b,1 -bag ) . x = 1 ) by A2, UPROOTS:8, UPROOTS:9;
hence ( x in a iff x in b ) by UPROOTS:8, UPROOTS:9; :: thesis: verum

end;

hence contradiction by A1, TARSKI:2; :: thesis: verum