let Gs be iterative eventually-constant ManySortedSet of NAT ; :: 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 that
A1: Gs .Lifespan() <= n and
A2: n <= m ; :: thesis: Gs . m = Gs . n
Gs . (Gs .Lifespan()) = Gs . m by A1, A2, Th9, XXREAL_0:2;
hence Gs . m = Gs . n by A1, Th9; :: thesis: verum