:: deftheorem defines -iterators FOMODEL4:def 9 :
for S being Language
for D being RuleSet of S holds D -iterators = { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;