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 :: thesis: for x being object st x in X holds
(b -' b) . x = (EmptyBag X) . x

let x be object ; :: 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 ; :: thesis: verum

end;

hence b -' b = EmptyBag X ; :: thesis: verum