for a being Integer holds
( ( a is even implies parity a is even ) & ( parity a is even implies a is even ) & ( parity a is even implies Parity a is even ) & ( Parity a is even implies parity a is even ) )