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

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 A2: ( m in dom (diameter S) & n in dom (diameter S) & m <= n ) ; :: thesis: (diameter S) . n >= (diameter S) . m
( S . m c= S . n & S . n is bounded & diameter (S . n) = (diameter S) . n & diameter (S . m) = (diameter S) . m ) by A1, A2, Def1, Def2, PROB_1:def 7;
hence (diameter S) . n >= (diameter S) . m by TBSP_1:32; :: thesis: verum

end;

hence diameter S is non-decreasing by SEQM_3:def 3; :: thesis: verum