theorem :: PNPROC_1:5

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