let M be non empty Reflexive MetrStruct ; :: thesis: for S being pointwise_bounded SetSequence of M holds diameter S is bounded_below
let S be pointwise_bounded SetSequence of M; :: thesis: diameter S is bounded_below
set d = diameter S;
now :: thesis: for n being Nat holds - 1 < (diameter S) . n
let n be Nat; :: thesis: - 1 < (diameter S) . n
A1: diameter (S . n) = (diameter S) . n by Def2;
S . n is bounded by Def1;
then 0 <= (diameter S) . n by A1, TBSP_1:21;
hence - 1 < (diameter S) . n by XXREAL_0:2; :: thesis: verum
end;
hence diameter S is bounded_below by SEQ_2:def 4; :: thesis: verum