let M be non empty Reflexive MetrStruct ; :: thesis: for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S
let S be finite Subset of M; :: thesis: diameter (M,(Complex_of {S})) = diameter S
set C = Complex_of {S};
reconsider C = Complex_of {S} as non void M bounded SimplicialComplex of M by Th6;
reconsider s = S as Subset of C ;
A1: the topology of C = bool S by SIMPLEX0:4;

now :: thesis: for W being Subset of M st W is Simplex of C holds
diameter W <= diameter S

let W be Subset of M; :: thesis: ( W is Simplex of C implies diameter W <= diameter S )
assume W is Simplex of C ; :: thesis: diameter W <= diameter S
then W in bool S by A1, PRE_TOPC:def 2;
hence diameter W <= diameter S by TBSP_1:24; :: thesis: verum

end;

then A2: diameter (M,C) <= diameter S by Def4;
S c= S ;
then s is simplex-like by A1, PRE_TOPC:def 2;
then diameter S <= diameter (M,C) by Def4;
hence diameter (M,(Complex_of {S})) = diameter S by A2, XXREAL_0:1; :: thesis: verum