:: deftheorem Def6 defines eventually-constant LEXBFS:def 7 :
for S being ManySortedSet of NAT holds
( S is eventually-constant iff ex n being Nat st
for m being Nat st n <= m holds
S . n = S . m );