let P be set ; :: thesis: for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m3 - m2 c= m3 - m1
let m1, m2, m3 be marking of P; :: thesis: ( m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1 )
assume that
A1: m1 c= m2 and
A2: m2 c= m3 ; :: thesis: m3 - m2 c= m3 - m1
A3: m1 c= m3 by A1, A2, Th2;
let p be set ; :: according to PNPROC_1:def 3 :: thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A4: p in P ; :: thesis: p multitude_of <= p multitude_of
then A5: m1 . p <= m2 . p by A1;
A6: (m3 - m1) . p = (m3 . p) - (m1 . p) by A3, A4, Def5;
(m3 - m2) . p = (m3 . p) - (m2 . p) by A2, A4, Def5;
hence p multitude_of <= p multitude_of by A5, A6, XREAL_1:10; :: thesis: verum