for n being Nat
for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r