let SK be SubSimplicialComplex of K; :: thesis: SK is M bounded
A1: the topology of SK c= the topology of K by SIMPLEX0:def 13;
consider r being Real such that
A2: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) by Def2;
take r ; :: according to SIMPLEX2:def 2 :: thesis: for A being Subset of M st A in the topology of SK holds
( A is bounded & diameter A <= r )
let A be Subset of M; :: thesis: ( A in the topology of SK implies ( A is bounded & diameter A <= r ) )
assume A in the topology of SK ; :: thesis: ( A is bounded & diameter A <= r )
hence ( A is bounded & diameter A <= r ) by A1, A2; :: thesis: verum