let M be non empty Reflexive MetrStruct ; :: thesis: for S being pointwise_bounded SetSequence of M st S is non-ascending holds
( diameter S is bounded_above & diameter S is non-increasing )
let S be pointwise_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 :: thesis: for n being Nat holds (diameter S) . n < ((diameter S) . 0) + 1

let n be Nat; :: thesis: (diameter S) . n < ((diameter S) . 0) + 1
A3: ((diameter S) . 0) + 0 < ((diameter S) . 0) + 1 by XREAL_1:8;
A4: diameter (S . n) = (diameter S) . n by Def2;
A5: diameter (S . 0) = (diameter S) . 0 by Def2;
A6: S . 0 is bounded by Def1;
S . n c= S . 0 by A1, PROB_1:def 4;
then (diameter S) . n <= (diameter S) . 0 by A6, A4, A5, TBSP_1:24;
hence (diameter S) . n < ((diameter S) . 0) + 1 by A3, XXREAL_0:2; :: thesis: verum

end;

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
A7: m <= n ; :: thesis: (diameter S) . n <= (diameter S) . m
A8: S . m is bounded by Def1;
A9: diameter (S . m) = (diameter S) . m by Def2;
A10: diameter (S . n) = (diameter S) . n by Def2;
S . n c= S . m by A1, A7, PROB_1:def 4;
hence (diameter S) . n <= (diameter S) . m by A8, A10, A9, TBSP_1:24; :: 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