:: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def 13 :
for X being set
for KX being SimplicialComplexStr of X
for b₃ being SimplicialComplex of X holds
( b₃ is SubSimplicialComplex of KX iff ( [#] b₃ c= [#] KX & the topology of b₃ c= the topology of KX ) );