theorem :: SIMPLEX0:53

for X being set
for KX being subset-closed SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree KX holds
ex S being Subset of KX st
( S is simplex-like & card S = n + 1 & BOOL S c= dom P & P .: (BOOL S) is Subset of KX & P | (BOOL S) is one-to-one ) ) holds
degree (subdivision (P,KX)) = degree KX