:: deftheorem defines diameter SIMPLEX2:def 6 :
for n being Nat
for K being SimplicialComplexStr of (TOP-REAL n) holds diameter K = diameter ((Euclid n),K);