theorem :: COUNTERS:5

for N being ExtNat holds 0 < N + 1 ;