let a, b be non zero Integer; :: thesis: ( Parity a > Parity b implies Parity (a + b) = Parity b )
assume A1: Parity a > Parity b ; :: thesis: Parity (a + b) = Parity b
then A1a: not Parity a divides Parity b by NAT_D:7;
A2: |.2.| > 1 ;
a <> - b by A1, PM;
then A3: a + b <> 0 ;
reconsider k = 2 |-count a as Nat ;
reconsider l = 2 |-count b as Nat ;
A2a: ( Parity a = 2 |^ k & Parity b = 2 |^ l ) by Def1;
then A2b: k > l by A1a, PEPIN:31;
then ( 2 |^ l divides Parity a & Parity a divides a & Parity b divides b ) by PEPIN:31, A2a, Th3;
then ( 2 |^ l divides a & 2 |^ l divides b ) by Def1, INT_2:9;
then A4: 2 |^ l divides a + b by WSIERP_1:4;
not 2 |^ (l + 1) divides a + b

proof

l + 1 <= k by A2b, NAT_1:13;
then B1: 2 |^ (l + 1) divides 2 |^ k by PEPIN:31;
2 |^ k divides a by A2, NEWTON03:def 7;
then B2: 2 |^ (l + 1) divides a by INT_2:9, B1;
not 2 |^ (l + 1) divides b by A2, NEWTON03:def 7;
hence not 2 |^ (l + 1) divides a + b by INT_2:1, B2; :: thesis: verum

end;

then 2 |-count (a + b) = l by A2, A3, A4, NEWTON03:def 7;
then Parity (a + b) = 2 |^ l by A3, Def1;
hence Parity (a + b) = Parity b by Def1; :: thesis: verum