theorem Th4: :: PNPROC_1:4

for P being set
for m1, m2 being marking of P holds m1 c= m1 + m2