theorem :: SIMPLEX0:45

for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i