:: deftheorem defines {$} PNPROC_1:def 2 :
for P being set holds {$} P = P --> 0;