A1: the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX) c= the topology of KX by Def2;
the_family_of KX is subset-closed ;
then ( [#] (Skeleton_of (KX,i)) = [#] KX & subset-closed_closure_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX)) c= the topology of KX ) by A1, Th3;
hence Skeleton_of (KX,i) is SubSimplicialComplex of KX by Def13; :: thesis: verum