theorem Th10: :: LEXBFS:10

for Gs being iterative eventually-constant ManySortedSet of NAT
for n, m being Nat st Gs .Lifespan() <= n & n <= m holds
Gs . m = Gs . n