let n be Nat; :: thesis: ex k being Nat st
( n = 2 * k or n = (2 * k) + 1 )

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: ex k being Nat st
( n = 2 * k or n = (2 * k) + 1 )

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

end;

suppose n is odd ; :: thesis: ex k being Nat st
( n = 2 * k or n = (2 * k) + 1 )

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: ( n = 2 * k or n = (2 * k) + 1 )
thus ( n = 2 * k or n = (2 * k) + 1 ) by A2; :: thesis: verum

end;

end;