let M be non empty Reflexive MetrStruct ; :: thesis: for S being bounded SetSequence of M holds diameter S is bounded_below
let S be bounded SetSequence of M; :: thesis: diameter S is bounded_below
set d = diameter S;

now

let n be Element of NAT ; :: thesis: - 1 < (diameter S) . n
( S . n is bounded & diameter (S . n) = (diameter S) . n ) by Def1, Def2;
then 0 <= (diameter S) . n by TBSP_1:29;
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