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
b + (EmptyBag X) = b by PRE_POLY:53;
hence b / b = EmptyBag X by Def1; :: thesis: verum