let P be set ; :: thesis: for m1, m2, m3 being marking of P st m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3
let m1, m2, m3 be marking of P; :: thesis: ( m1 c= m2 implies (m2 + m3) - m1 = (m2 - m1) + m3 )
assume A1: m1 c= m2 ; :: thesis: (m2 + m3) - m1 = (m2 - m1) + m3
let p be object ; :: according to PNPROC_1:def 1 :: thesis: ( p in P implies p multitude_of = p multitude_of )
assume A2: p in P ; :: thesis: p multitude_of = p multitude_of
m2 c= m2 + m3 by Th4;
then A3: m1 c= m2 + m3 by A1, Th2;
((m2 - m1) + m3) . p = ((m2 - m1) . p) + (m3 . p) by A2, Def4
.= (m3 . p) + ((m2 . p) - (m1 . p)) by A1, A2, Def5
.= ((m3 . p) + (m2 . p)) - (m1 . p)
.= ((m3 + m2) . p) - (m1 . p) by A2, Def4
.= ((m2 + m3) - m1) . p by A2, A3, Def5 ;
hence p multitude_of = p multitude_of ; :: thesis: verum