theorem Th16: :: SIMPLEX2:16

for n being Nat
for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)