let P be set ; for m1, m2, m3 being marking of P st m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)
let m1, m2, m3 be marking of P; ( m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3) )
assume
m2 + m3 c= m1
; (m1 - m2) - m3 = m1 - (m2 + m3)
then (m1 - m2) - m3 =
(((m1 - (m2 + m3)) + (m2 + m3)) - m2) - m3
by Th15
.=
((((m1 - (m2 + m3)) + m3) + m2) - m2) - m3
by Th11
.=
((m1 - (m2 + m3)) + m3) - m3
by Th16
.=
m1 - (m2 + m3)
by Th16
;
hence
(m1 - m2) - m3 = m1 - (m2 + m3)
; verum