theorem :: COUNTERS:26

for X being ext-natural-membered set
for Y being set st Y c= X holds
Y is ext-natural-membered ;