theorem :: COUNTERS:10

for N, M being ExtNat st N + M = 0 holds
( N = 0 & M = 0 ) ;