set C = Complex_of (the_subsets_with_limited_card (i + 1),the topology of KX);
[#] KX c= X by Def9;
then [#] (Complex_of (the_subsets_with_limited_card (i + 1),the topology of KX)) c= X ;
hence Complex_of (the_subsets_with_limited_card (i + 1),the topology of KX) is SimplicialComplexStr of X by Def9; :: thesis: verum