let P be set ; for m2, m3, m1 being marking of P st m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)
let m2, m3, m1 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 Th27
.=
((((m1 - (m2 + m3)) + m3) + m2) - m2) - m3
by Th23
.=
((m1 - (m2 + m3)) + m3) - m3
by Th28
.=
m1 - (m2 + m3)
by Th28
;
hence
(m1 - m2) - m3 = m1 - (m2 + m3)
; verum