let a, b be Integer; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

per cases ( a is even or a is odd ) ;

suppose A1: a is even ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

per cases ( b is even or b is odd ) ;

suppose b is even ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

then ( parity (a - b) = 0 & |.((parity a) - (parity b)).| = 0 ) by A1;
hence parity (a - b) = |.((parity a) - (parity b)).| ; :: thesis: verum

end;

suppose B1: b is odd ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

then B2: a - b is odd by A1;
|.((parity a) - (parity b)).| = - (- 1) by A1, B1
.= parity (a - b) by B2 ;
hence parity (a - b) = |.((parity a) - (parity b)).| ; :: thesis: verum

end;

end;

end;

suppose A1: a is odd ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

per cases ( b is odd or b is even ) ;

suppose b is odd ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

then ( parity (a - b) = 0 & |.((parity a) - (parity b)).| = 0 ) by A1;
hence parity (a - b) = |.((parity a) - (parity b)).| ; :: thesis: verum

end;

suppose B1: b is even ; :: thesis: parity (a - b) = |.((parity a) - (parity b)).|

then a - b is odd by A1;
hence parity (a - b) = |.((parity a) - (parity b)).| by A1, B1; :: thesis: verum

end;

end;

end;

end;