( ( a = 0 or a is non zero even Integer ) & Parity 0 is even ) by Def1;
hence Parity a is even ; :: thesis: verum