let X be set ; :: thesis: for b being bag of X holds b -' b = EmptyBag X
let b be bag of X; :: thesis: b -' b = EmptyBag X

now

let x be set ; :: thesis: ( x in X implies (b -' b) . x = (EmptyBag X) . x )
assume x in X ; :: thesis: (b -' b) . x = (EmptyBag X) . x
thus (b -' b) . x = (b . x) -' (b . x) by Def6
.= 0 by XREAL_1:232
.= (EmptyBag X) . x by Th52 ; :: thesis: verum

end;

hence b -' b = EmptyBag X by PBOOLE:3; :: thesis: verum