:: deftheorem Def4 defines + PNPROC_1:def 4 :
for P being set
for m1, m2, b₄ being marking of P holds
( b₄ = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) );