:: deftheorem Def5 defines iterative LEXBFS:def 6 :
for s being ManySortedSet of NAT holds
( s is iterative iff for k, n being Nat st s . k = s . n holds
s . (k + 1) = s . (n + 1) );