let a be Nat; :: thesis: Parity (a + (Parity a)) >= 2 * (Parity a)

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: Parity (a + (Parity a)) >= 2 * (Parity a)

then Parity a = 0 by Def1;
hence Parity (a + (Parity a)) >= 2 * (Parity a) ; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: Parity (a + (Parity a)) >= 2 * (Parity a)

hence Parity (a + (Parity a)) >= 2 * (Parity a) by ADA, NAT_D:7; :: thesis: verum

end;

end;