theorem Th16: :: PNPROC_1:16

for P being set
for m1, m2 being marking of P holds (m1 + m2) - m1 = m2