theorem Th54: :: SIMPLEX0:54

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