let P be set ; :: thesis: for m1, m2, m3 being marking of P st m3 c= m2 & m2 c= m1 holds
m1 - (m2 - m3) = (m1 - m2) + m3
let m1, m2, m3 be marking of P; :: thesis: ( m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3 )
assume A1: m3 c= m2 ; :: thesis: ( not m2 c= m1 or m1 - (m2 - m3) = (m1 - m2) + m3 )
assume A2: m2 c= m1 ; :: thesis: m1 - (m2 - m3) = (m1 - m2) + m3
A3: m2 - m3 c= m3 + (m2 - m3) by Th4;
A4: m2 = m3 + (m2 - m3) by A1, Th15;
then (m3 + (m2 - m3)) - (m2 - m3) c= m1 - (m2 - m3) by A2, A3, Th14;
then A5: m3 c= m1 - (m2 - m3) by Th16;
thus (m1 - m2) + m3 = ((m1 - (m2 - m3)) - m3) + m3 by A2, A4, Th17
.= m1 - (m2 - m3) by A5, Th15 ; :: thesis: verum