theorem :: PNPROC_1:18

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