theorem :: PNPROC_1:3

for P being set
for m being marking of P holds m + ({$} P) = m