theorem Th4c: :: COUNTERS:16

for N being ExtNat st N < 1 holds
N = 0