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