let a, b be Integer; :: thesis: ( a + b is even iff parity a = parity b )
thus ( a + b is even implies parity a = parity b ) :: thesis: ( parity a = parity b implies a + b is even )

proof

assume a + b is even ; :: thesis: parity a = parity b
then 0 = parity (a + b)
.= |.((parity a) - (parity b)).| by ABP ;
then (parity a) - (parity b) = 0 ;
hence parity a = parity b ; :: thesis: verum

end;

assume parity a = parity b ; :: thesis: a + b is even
then 0 = |.((parity a) - (parity b)).|
.= parity (a + b) by ABP ;
hence a + b is even ; :: thesis: verum