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