theorem Th4: :: PNPROC_1:4
for P being set
for m1, m2 being marking of P holds m1 c= m1 + m2