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

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