theorem Th8: :: LEXBFS:8

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