:: deftheorem defines Skeleton_of SIMPLEX0:def 17 :
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number holds Skeleton_of (KX,i) = Complex_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX));