let n be set ; :: thesis: for b1, b2 being bag of st b1 divides b2 & b2 -' b1 = EmptyBag n holds
b2 = b1
let b1, b2 be bag of ; :: thesis: ( b1 divides b2 & b2 -' b1 = EmptyBag n implies b2 = b1 )
assume that
A1: b1 divides b2 and
A2: b2 -' b1 = EmptyBag n ; :: thesis: b2 = b1

now

let k be set ; :: thesis: ( k in n implies b2 . k = b1 . k )
assume k in n ; :: thesis: b2 . k = b1 . k
A3: b1 . k <= b2 . k by A1, Def13;
0 = (b2 -' b1) . k by A2, Th56
.= (b2 . k) -' (b1 . k) by Def6 ;
then b2 . k <= b1 . k by NAT_D:36;
hence b2 . k = b1 . k by A3, XXREAL_0:1; :: thesis: verum

end;

hence b2 = b1 by PBOOLE:3; :: thesis: verum