let Gs be iterative eventually-constant ManySortedSet of ; :: thesis: for n, m being Nat st Gs .Lifespan() <= n & n <= m holds
Gs . m = Gs . n
let n, m be Nat; :: thesis: ( Gs .Lifespan() <= n & n <= m implies Gs . m = Gs . n )
assume A1: ( Gs .Lifespan() <= n & n <= m ) ; :: thesis: Gs . m = Gs . n
Gs . (Gs .Lifespan() ) = Gs . m by A1, Th16, XXREAL_0:2;
hence Gs . m = Gs . n by A1, Th16; :: thesis: verum