let a, b be Integer; :: thesis: ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b )

per cases ( a is zero or b is zero or ( not a is zero & not b is zero ) ) ;

suppose a is zero ; :: thesis: ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b )

then ( Parity (a + b) = Parity b & Parity a = 0 ) by Def1;
hence ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b ) ; :: thesis: verum

end;

suppose b is zero ; :: thesis: ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b )

then ( Parity (a + b) = Parity a & Parity b = 0 ) by Def1;
hence ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b ) ; :: thesis: verum

end;

suppose ( not a is zero & not b is zero ) ; :: thesis: ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b )

hence ( Parity (a + b) > (Parity a) + (Parity b) implies Parity a = Parity b ) by LEQ; :: thesis: verum

end;

end;