let a, b be Integer; :: thesis: parity (a + b) = |.((parity a) - (parity b)).|
thus parity (a + b) = parity (a - b) by PPM
.= |.((parity a) - (parity b)).| by PMI ; :: thesis: verum