let n be Nat; :: thesis: ( n is odd iff n mod 2 = 1 )
( n is odd iff not n mod 2 = 0 ) by Th21;
hence ( n is odd iff n mod 2 = 1 ) by NAT_D:12; :: thesis: verum