let a, b be Nat; :: thesis: ( ( parity (a + b) = parity b implies parity a = 0 ) & ( parity (a + b) <> parity b implies parity a = 1 ) )
( ( (a + b) mod 2 = b mod 2 implies a mod 2 = 0 ) & ( (a + b) mod 2 <> b mod 2 implies a mod 2 <> 0 ) ) by MAB;
hence ( ( parity (a + b) = parity b implies parity a = 0 ) & ( parity (a + b) <> parity b implies parity a = 1 ) ) by NAT_2:def 1; :: thesis: verum