let a be Integer; :: thesis: ( ( 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 ) )

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

suppose a is even ; :: thesis: ( ( 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 ) )

hence ( ( 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 ) ) ; :: thesis: verum

end;

suppose a is odd ; :: thesis: ( ( 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 ) )

hence ( ( 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 ) ) ; :: thesis: verum

end;

end;