for X being set
for M being non empty Reflexive MetrStruct
for K being b₂ bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)