for N being ExtNat holds 0 < N + 1 ;