theorem Lem14: :: BAGORD_2:63

for I being set
for p being Bags b₁ -valued FinSequence
for x being object st x in I & (Sum p) . x > 0 holds
ex i being Nat st
( i in dom p & (p /. i) . x > 0 )