:: deftheorem defines = COUNTERS:def 5 :
for X, Y being ext-natural-membered set holds
( X = Y iff for N being ExtNat holds
( N in X iff N in Y ) );