let M be non empty Reflexive MetrStruct ; :: thesis: for S being bounded SetSequence of M st S is non-ascending holds
( diameter S is bounded_above & diameter S is non-increasing )
let S be bounded SetSequence of M; :: thesis: ( S is non-ascending implies ( diameter S is bounded_above & diameter S is non-increasing ) )
assume A1: S is non-ascending ; :: thesis: ( diameter S is bounded_above & diameter S is non-increasing )
set d = diameter S;

A2: now

let n be Element of NAT ; :: thesis: (diameter S) . n < ((diameter S) . 0 ) + 1
( S . n c= S . 0 & S . 0 is bounded & diameter (S . n) = (diameter S) . n & diameter (S . 0 ) = (diameter S) . 0 ) by A1, Def1, Def2, PROB_1:def 6;
then ( (diameter S) . n <= (diameter S) . 0 & ((diameter S) . 0 ) + 0 < ((diameter S) . 0 ) + 1 ) by TBSP_1:32, XREAL_1:10;
hence (diameter S) . n < ((diameter S) . 0 ) + 1 by XXREAL_0:2; :: thesis: verum

end;

now

let m, n be Element of NAT ; :: thesis: ( m in dom (diameter S) & n in dom (diameter S) & m <= n implies (diameter S) . n <= (diameter S) . m )
assume A3: ( m in dom (diameter S) & n in dom (diameter S) & m <= n ) ; :: thesis: (diameter S) . n <= (diameter S) . m
( S . n c= S . m & S . m is bounded & diameter (S . n) = (diameter S) . n & diameter (S . m) = (diameter S) . m ) by A1, A3, Def1, Def2, PROB_1:def 6;
hence (diameter S) . n <= (diameter S) . m by TBSP_1:32; :: thesis: verum

end;

hence ( diameter S is bounded_above & diameter S is non-increasing ) by A2, SEQM_3:def 4, SEQ_2:def 3; :: thesis: verum