theorem bag2: :: FIELD_14:10

for R being domRing
for B1 being bag of the carrier of R holds
( card B1 = 1 iff ex a being Element of R st B1 = Bag {a} )