let P be set ; :: thesis: for m1, m2, m being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m
let m1, m2, m 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 3 :: 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, Th2;
m1 . p <= m2 . p by A2, A3;
then (m1 . p) - (m . p) <= (m2 . p) - (m . p) by XREAL_1:9;
then (m1 - m) . p <= (m2 . p) - (m . p) by A1, A3, Def5;
hence p multitude_of <= p multitude_of by A3, A4, Def5; :: thesis: verum