:: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def 9 :
for X being set
for b₂ being SimplicialComplexStr holds
( b₂ is SimplicialComplexStr of X iff [#] b₂ c= X );