theorem Th52: :: SIMPLEX0:52

for X being set
for KX being SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX