theorem Th7: :: PNPROC_1:7

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