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