let K be SimplicialComplexStr of (TOP-REAL n); :: thesis: ( K is finite-vertices implies K is bounded )
assume K is finite-vertices ; :: thesis: K is bounded
then K is Euclid n bounded by Th6;
hence K is bounded by Def5; :: thesis: verum