let n be natural odd number ; :: thesis: 1 <= n
2 * 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
hence 1 <= n ; :: thesis: verum