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