theorem Th3: :: COUNTERS:2

for x being object holds
( x is ExtNat iff ( x is Nat or x = +infty ) )