theorem :: PNPROC_1:10

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