let n be Nat; :: thesis: 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
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); :: thesis: ( |.K.| c= [#] K implies for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r )
assume A1: |.K.| c= [#] K ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
set dK = degree K;
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st diameter (BCS (k,K)) < r )
assume A2: r > 0 ; :: thesis: ex k being Nat st diameter (BCS (k,K)) < r
set ddK = (degree K) / ((degree K) + 1);

per cases ( degree K = 0 or degree K = - 1 or diameter K = 0 or ( degree K <> 0 & degree K <> - 1 & diameter K <> 0 ) ) ;

suppose ( degree K = 0 or degree K = - 1 ) ; :: thesis: ex k being Nat st diameter (BCS (k,K)) < r

then A3: (degree K) / ((degree K) + 1) = 0 ;
( diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) & BCS K = BCS (1,K) ) by A1, Th16, SIMPLEX1:17;
hence ex k being Nat st diameter (BCS (k,K)) < r by A2, A3; :: thesis: verum

end;

suppose A4: diameter K = 0 ; :: thesis: ex k being Nat st diameter (BCS (k,K)) < r

K = BCS (0,K) by A1, SIMPLEX1:16;
hence ex k being Nat st diameter (BCS (k,K)) < r by A2, A4; :: thesis: verum

end;

suppose A5: ( degree K <> 0 & degree K <> - 1 & diameter K <> 0 ) ; :: thesis: ex k being Nat st diameter (BCS (k,K)) < r

degree K >= - 1 by SIMPLEX0:23;
then degree K > - 1 by A5, XXREAL_0:1;
then A6: degree K >= (- 1) + 1 by INT_1:7;
then A7: (degree K) / ((degree K) + 1) > 0 by A5, XREAL_1:139;
(degree K) + 1 > degree K by XREAL_1:29;
then A8: (degree K) / ((degree K) + 1) < 1 by A6, XREAL_1:189;
A9: diameter K > 0 by A5, Th7;
then r / (diameter K) > 0 by A2, XREAL_1:139;
then consider k being Nat such that
A10: ((degree K) / ((degree K) + 1)) to_power k < r / (diameter K) by A7, A8, TBSP_1:3;
A11: (r / (diameter K)) * (diameter K) = r by A5, XCMPLX_1:87;
A12: diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) by A1, Th17;
((degree K) / ((degree K) + 1)) to_power k = ((degree K) / ((degree K) + 1)) |^ k by POWER:41;
then (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) < r by A9, A10, A11, XREAL_1:68;
then diameter (BCS (k,K)) < r by A12, XXREAL_0:2;
hence ex k being Nat st diameter (BCS (k,K)) < r ; :: thesis: verum

end;

end;