for i, j being Nat st i is odd & j is odd holds
i * j is odd ;