:: deftheorem defines locally-finite SIMPLEX0:def 6 :
for K being SimplicialComplexStr holds
( K is locally-finite iff for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite );