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