:: deftheorem Def4 defines Vertices SIMPLEX0:def 4 :
for K being SimplicialComplexStr
for b₂ being Subset of K holds
( b₂ = Vertices K iff for v being Element of K holds
( v in b₂ iff v is vertex-like ) );