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 = {} )

( 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;then b = EmptyBag X by PRE_POLY:81;

hence card b = 0 by UPROOTS:11; :: thesis: verum

now :: thesis: ( card b = 0 implies support b = {} )

hence
( card b = 0 iff support b = {} )
by A; :: thesis: verumassume
card b = 0
; :: thesis: support b = {}

then b = EmptyBag X by UPROOTS:12;

hence support b = {} ; :: thesis: verum

end;then b = EmptyBag X by UPROOTS:12;

hence support b = {} ; :: thesis: verum