A1: the_subsets_with_limited_card ((i + 1), the topology of KX) c= the topology of KX

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_with_limited_card ((i + 1), the topology of KX) or x in the topology of KX )
assume x in the_subsets_with_limited_card ((i + 1), the topology of KX) ; :: thesis: x in the topology of KX
hence x in the topology of KX by Def2; :: thesis: verum

end;

the_family_of KX is subset-closed ;
then ( [#] (Skeleton_of (KX,i)) = [#] KX & subset-closed_closure_of (the_subsets_with_limited_card ((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