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