:: deftheorem defines bounded SIMPLEX2:def 5 :
for n being Nat
for K being SimplicialComplexStr of (TOP-REAL n) holds
( K is bounded iff K is Euclid n bounded );