let P be set ; :: thesis: for m1, m2 being marking of P st m1 c= m2 holds
m2 - m1 c= m2
let m1, m2 be marking of P; :: thesis: ( m1 c= m2 implies m2 - m1 c= m2 )
assume A1: m1 c= m2 ; :: thesis: m2 - m1 c= 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 A2: (m2 - m1) . p = (m2 . p) - (m1 . p) by A1, Def5;
(m2 . p) - 0 = m2 . p ;
hence p multitude_of <= p multitude_of by A2, XREAL_1:13; :: thesis: verum