let P be set ; :: thesis: for m, m1, m2 being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m
let m, m1, m2 be marking of P; :: thesis: ( m c= m1 & m1 c= m2 implies m1 - m c= m2 - m )
assume A1: m c= m1 ; :: thesis: ( not m1 c= m2 or m1 - m c= m2 - m )
assume A2: m1 c= m2 ; :: thesis: m1 - m c= m2 - m
let p be set ; :: according to PNPROC_1:def 4 :: thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A3: p in P ; :: thesis: p multitude_of <= p multitude_of
A4: m c= m2 by A1, A2, Th14;
m1 . p <= m2 . p by A2, A3, Def4;
then (m1 . p) - (m . p) <= (m2 . p) - (m . p) by XREAL_1:11;
then (m1 - m) . p <= (m2 . p) - (m . p) by A1, A3, Def6;
hence p multitude_of <= p multitude_of by A3, A4, Def6; :: thesis: verum