let n be natural Number ; :: thesis: ( n mod 2 = 0 or n mod 2 = 1 )
assume A1: n mod 2 <> 0 ; :: thesis: n mod 2 = 1
A2: 2 = 1 + 1 ;
n mod 2 < 2 by Th1;
then A3: n mod 2 <= 1 by A2, NAT_1:13;
n mod 2 >= 1 by A1, NAT_1:14;
hence n mod 2 = 1 by A3, XXREAL_0:1; :: thesis: verum