let P be set ; :: thesis: for m1, m2 being marking of P holds m1 c= m1 + m2
let m1, m2 be marking of P; :: thesis: m1 c= m1 + m2
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 multitude_of = (p multitude_of ) + (p multitude_of ) by Def4;
hence p multitude_of <= p multitude_of by NAT_1:11; :: thesis: verum