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

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