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