theorem :: SIMPLEX0:31

for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX