let X be non empty set ; :: thesis: for b being bag of X holds
( card b = 0 iff support b = {} )
let b be bag of X; :: thesis: ( card b = 0 iff support b = {} )
A: now :: thesis: ( support b = {} implies card b = 0 )
assume support b = {} ; :: thesis: card b = 0
then b = EmptyBag X by PRE_POLY:81;
hence card b = 0 by UPROOTS:11; :: thesis: verum
end;
now :: thesis: ( card b = 0 implies support b = {} )
assume card b = 0 ; :: thesis: support b = {}
then b = EmptyBag X by UPROOTS:12;
hence support b = {} ; :: thesis: verum
end;
hence ( card b = 0 iff support b = {} ) by A; :: thesis: verum