theorem :: COUNTERS:4

for N being ExtNat st 0 <> N holds
0 < N ;