theorem Th3: :: SIMPLEX1:3

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