for N being ExtNat holds 0 <= N ;