theorem Th7: :: LEXBFS:7

for Gs being ManySortedSet of NAT st Gs is halting & Gs is iterative holds
Gs is eventually-constant