theorem bag2b: :: FIELD_14:9

for Z being non empty set
for B being bag of Z
for o1, o2 being object st B . o1 = card B & o2 <> o1 holds
B . o2 = 0