for X, Y, Z being set
for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX)