for X being 1-sorted
for K being subset-closed SimplicialComplexStr of X st K is total holds
for S being finite Subset of K st S is simplex-like holds
Complex_of {(@ S)} is SubSimplicialComplex of K