let X be set ; :: thesis: for b being bag of holds b / b = EmptyBag X
let b be bag of ; :: thesis: b / b = EmptyBag X
b + (EmptyBag X) = b by PRE_POLY:53;
hence b / b = EmptyBag X by Def1; :: thesis: verum