theorem ThSubset: :: COUNTERS:23

for X being set holds
( X is ext-natural-membered iff X c= ExtNAT )