:: deftheorem Def5 defines finite-vertices SIMPLEX0:def 5 :
for K being SimplicialComplexStr holds
( K is finite-vertices iff Vertices K is finite );