let P be set ; :: thesis: for m being marking of P holds {$} P c= m
let m be marking of P; :: thesis: {$} P c= m
let p be set ; :: according to PNPROC_1:def 3 :: thesis: ( p in P implies p multitude_of <= p multitude_of )
assume p in P ; :: thesis: p multitude_of <= p multitude_of
then ({$} P) . p = 0 by Lm7;
hence p multitude_of <= p multitude_of by NAT_1:2; :: thesis: verum