theorem ThEx: :: COUNTERS:24

for X being non empty ext-natural-membered set ex N being ExtNat st N in X