let M be non empty Reflexive MetrStruct ; :: thesis: for K being SimplicialComplexStr st K is finite-vertices holds
K is M bounded
let K be SimplicialComplexStr; :: thesis: ( K is finite-vertices implies K is M bounded )
set V = Vertices K;
assume K is finite-vertices ; :: thesis: K is M bounded
then Vertices K is finite ;
then reconsider VM = (Vertices K) /\ ([#] M) as finite Subset of M ;
take diameter VM ; :: according to SIMPLEX2:def 2 :: thesis: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= diameter VM )
let A be Subset of M; :: thesis: ( A in the topology of K implies ( A is bounded & diameter A <= diameter VM ) )
assume A1: A in the topology of K ; :: thesis: ( A is bounded & diameter A <= diameter VM )
then reconsider S = A as Subset of K ;
S is simplex-like by A1, PRE_TOPC:def 2;
then A c= Vertices K by SIMPLEX0:17;
then A c= VM by XBOOLE_1:19;
hence ( A is bounded & diameter A <= diameter VM ) by TBSP_1:24; :: thesis: verum