:: deftheorem Def15 defines | SIMPLEX0:def 15 :
for X being set
for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX st (bool A) /\ the topology of KX is finite-membered holds
for b₄ being strict maximal SubSimplicialComplex of KX holds
( b₄ = KX | A iff [#] b₄ = A );