:: deftheorem Def16 defines | SIMPLEX0:def 16 :
for X being set
for SC being SimplicialComplex of X
for A being Subset of SC
for b₄ being strict maximal SubSimplicialComplex of SC holds
( b₄ = SC | A iff [#] b₄ = A );