let a be Nat; :: thesis: ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
set b = a div 2;
set d = a mod 2;
a = (2 * (a div 2)) + (a mod 2) by NAT_D:2;
then ( a = (2 * (a div 2)) + 0 or a = (2 * (a div 2)) + 1 ) by NAT_1:23, NAT_D:1;
hence ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 ) ; :: thesis: verum