let M be non empty Reflexive MetrStruct ; :: thesis: for S being pointwise_bounded SetSequence of M st S is non-descending holds
diameter S is non-decreasing
let S be pointwise_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 :: thesis: for m, n being Nat st m in dom (diameter S) & n in dom (diameter S) & m <= n holds
(diameter S) . n >= (diameter S) . m

let m, n be Nat; :: thesis: ( m in dom (diameter S) & n in dom (diameter S) & m <= n implies (diameter S) . n >= (diameter S) . m )
assume that
m in dom (diameter S) and
n in dom (diameter S) and
A2: m <= n ; :: thesis: (diameter S) . n >= (diameter S) . m
A3: S . n is bounded by Def1;
A4: diameter (S . m) = (diameter S) . m by Def2;
A5: diameter (S . n) = (diameter S) . n by Def2;
S . m c= S . n by A1, A2, PROB_1:def 5;
hence (diameter S) . n >= (diameter S) . m by A3, A5, A4, TBSP_1:24; :: thesis: verum

end;

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