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: lim_sup S = A by A1, Th17;
A3: lim_inf S = A by A1, Th18;

A4: now

let n be Element of NAT ; :: thesis: S . n c= S . (n + 1)
( S . n = A & S . (n + 1) = A ) by A1;
hence S . n c= S . (n + 1) ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: S . (n + 1) c= S . n
( S . n = A & S . (n + 1) = A ) by A1;
hence S . (n + 1) c= S . n ; :: thesis: verum

end;

hence ( S is convergent & S is non-descending & S is non-ascending ) by A2, A3, A4, Def5, Def6, Def7; :: thesis: verum