theorem Th1: :: PNPROC_1:1

for P being set
for m being marking of P holds {$} P c= m by Lm1;