theorem :: COUNTERS:3

for N being ExtNat holds 0 <= N ;