let a be Integer; :: thesis: Parity a divides a

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: Parity a divides a

hence Parity a divides a by Def1; :: thesis: verum

end;

suppose A1: a <> 0 ; :: thesis: Parity a divides a

|.2.| > 1 ;
then 2 |^ (2 |-count a) divides a by A1, NEWTON03:def 7;
hence Parity a divides a by A1, Def1; :: thesis: verum

end;

end;