let a, b be non zero Integer; :: thesis: ( a + b <> 0 & Parity a = Parity b & parity ((Oddity a) div 2) <> parity ((Oddity b) div 2) implies Parity (a + b) > (Parity a) + (Parity b) )
assume A1: ( a + b <> 0 & Parity a = Parity b & parity ((Oddity a) div 2) <> parity ((Oddity b) div 2) ) ; :: thesis: Parity (a + b) > (Parity a) + (Parity b)
A2: Parity (a + b) >= (Parity a) + (Parity b) by A1, PEQ;
Parity (a + b) <> (Parity a) + (Parity b) by A1, PSU;
hence Parity (a + b) > (Parity a) + (Parity b) by A2, XXREAL_0:1; :: thesis: verum