theorem :: SIMPLEX0:41

for X being set
for KX being SimplicialComplexStr of X
for i1, i2 being dim-like number st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)