theorem :: SIMPLEX0:43

for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number holds degree (Skeleton_of (KX,i)) <= degree KX