theorem Th9: :: PNPROC_1:9

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