let a, b be non zero Integer; :: thesis: ( a + b <> 0 & Parity (a + b) = Parity a implies Parity a < Parity b )
assume A0: a + b <> 0 ; :: thesis: ( not Parity (a + b) = Parity a or Parity a < Parity b )
assume A1: Parity (a + b) = Parity a ; :: thesis: Parity a < Parity b
(Parity a) + (Parity b) > (Parity a) + 0 by XREAL_1:6;
then Parity a <> Parity b by A0, A1, PEQ;
then ( Parity a > Parity b or Parity a < Parity b ) by XXREAL_0:1;
hence Parity a < Parity b by PAP, A1; :: thesis: verum