let n be Nat; 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
;
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
;
( n = 2 * k or n = (2 * k) + 1 )thus
(
n = 2
* k or
n = (2 * k) + 1 )
by A1;
verum end; suppose
n is
odd
;
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
;
( n = 2 * k or n = (2 * k) + 1 )thus
(
n = 2
* k or
n = (2 * k) + 1 )
by A2;
verum end; end;