theorem :: SIMPLEX0:57

for X, Y being set
for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)