theorem Th15: :: PNPROC_1:15

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