let n be Nat; :: thesis:

per cases ;

suppose n is even ; :: thesis:

then consider k being Nat such that
A1: n = 2 * k ;
take k ; :: thesis:
thus ( n = 2 * k or n = (2 * k) + 1 ) by A1; :: thesis:

end;

suppose n is odd ; :: thesis:

then n + 1 is even ;
then consider k1 being Nat such that
A2: n + 1 = 2 * k1 ;
0 <> k1 by A2;
then reconsider k = k1 - 1 as Nat ;
take k ; :: thesis:
thus ( n = 2 * k or n = (2 * k) + 1 ) by A2; :: thesis:

end;

end;