theorem :: PNPROC_1:12

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