for X being set
for KX being SimplicialComplexStr of X
for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1