let a be Integer; :: thesis: ( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) )

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

suppose a is zero ; :: thesis: ( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) )

then Parity a = 0 by Def1;
hence ( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) ) ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: ( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) )

then reconsider a = a as non zero Integer ;
( 2 divides Parity ((Oddity a) + 1) & 2 divides Parity ((Oddity a) - 1) ) by ABIAN:def 1;
then ( 2 * (Parity a) divides (Parity a) * (Parity ((Oddity a) + 1)) & 2 * (Parity a) divides (Parity a) * (Parity ((Oddity a) - 1)) ) by NEWTON03:5;
hence ( 2 * (Parity a) divides Parity (a + (Parity a)) & 2 * (Parity a) divides Parity (a - (Parity a)) ) by PGP; :: thesis: verum

end;

end;