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