per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: Parity (Oddity a) is trivial

hence Parity (Oddity a) is trivial by Def1; :: thesis: verum

end;

suppose not a is zero ; :: thesis: Parity (Oddity a) is trivial

then reconsider a = a as non zero Integer ;
( Oddity (Oddity a) = Oddity a & (Oddity (Oddity a)) * (Parity (Oddity a)) = Oddity a ) ;
hence Parity (Oddity a) is trivial by XCMPLX_1:7; :: thesis: verum

end;

end;