let M be non empty Reflexive MetrStruct ; :: thesis: for A being Subset of M
for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds
A is bounded
let A be Subset of M; :: thesis: for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds
A is bounded
let K be non void SimplicialComplexStr; :: thesis: ( K is M bounded & A is Simplex of K implies A is bounded )
assume K is M bounded ; :: thesis: ( not A is Simplex of K or A is bounded )
then A1: ex r being Real st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) ;
assume A is Simplex of K ; :: thesis: A is bounded
then A in the topology of K by PRE_TOPC:def 2;
hence A is bounded by A1; :: thesis: verum