let X be non empty set ; :: thesis: for b being bag of X holds
( b is zero iff support b = {} )
let b be bag of X; :: thesis: ( b is zero iff support b = {} )

now :: thesis: ( support b = {} implies b is zero )

assume support b = {} ; :: thesis: b is zero
then for o being object st o in X holds
b . o = {} by PRE_POLY:def 7;
hence b is zero by PBOOLE:6; :: thesis: verum

end;

hence ( b is zero iff support b = {} ) ; :: thesis: verum