theorem Th17: :: PNPROC_1:17

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