let P be set ; 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; ( m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3 )
assume A1:
m1 c= m2
; ( not m3 c= m4 or not m4 c= m1 or m1 - m4 c= m2 - m3 )
assume A2:
m3 c= m4
; ( not m4 c= m1 or m1 - m4 c= m2 - m3 )
assume A3:
m4 c= m1
; m1 - m4 c= m2 - m3
then
m4 c= m2
by A1, Th2;
then A4:
m3 c= m2
by A2, Th2;
let p be set ; PNPROC_1:def 3 ( p in P implies p multitude_of <= p multitude_of )
assume A5:
p in P
; 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; verum