:: deftheorem Def5 defines - PNPROC_1:def 5 :
for P being set
for m1, m2 being marking of P st m2 c= m1 holds
for 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 ) );