theorem Th60: :: SIMPLEX0:60

for X being set
for P being Function
for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)