let a be Nat; :: thesis: ( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a )

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

suppose a = Parity a ; :: thesis: ( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a )

hence ( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a ) ; :: thesis: verum

end;

suppose A0: a <> Parity a ; :: thesis: ( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a )

then reconsider a = a as non zero Nat by Def1;
A1: Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) by PGP;
a = (Oddity a) * (Parity a) ;
then A2: (Oddity a) - 1 <> 0 by A0;
Parity ((Oddity a) - 1) <> 1 ;
hence ( Parity (a - (Parity a)) >= 2 * (Parity a) or a = Parity a ) by A1, A2, XREAL_1:64, NAT_1:23; :: thesis: verum

end;

end;