for n being Nat holds
( n is odd iff n mod 2 = 1 ) by Th21, NAT_D:12;