theorem :: PNPROC_1:13

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