let S be SetSequence of T; :: thesis: ( S is constant implies ( S is convergent & S is non-descending & S is non-ascending ) )
assume S is constant ; :: thesis: ( S is convergent & S is non-descending & S is non-ascending )
then consider A being Subset of T such that
A1: for n being Nat holds S . n = A by VALUED_0:def 18;

A2: now :: thesis: for n being Nat holds S . (n + 1) c= S . n

let n be Nat; :: thesis: S . (n + 1) c= S . n
S . n = A by A1;
hence S . (n + 1) c= S . n by A1; :: thesis: verum

end;

A3: now :: thesis: for n being Nat holds S . n c= S . (n + 1)

let n be Nat; :: thesis: S . n c= S . (n + 1)
S . n = A by A1;
hence S . n c= S . (n + 1) by A1; :: thesis: verum

end;

( lim_sup S = A & lim_inf S = A ) by A1, Th14, Th15;
hence ( S is convergent & S is non-descending & S is non-ascending ) by A3, A2; :: thesis: verum