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