theorem :: COUNTERS:29
for R being Relation
for S being ext-natural-valued Relation st R c= S holds
R is ext-natural-valued ;