theorem :: SIMPLEX0:59

for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A