reconsider i1 = i + 1 as Integer ;
set SUB = the_subsets_with_limited_card ((i + 1), the topology of KX);
set C = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));

now

let A be finite Subset of (Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX))); :: thesis: ( A is simplex-like implies card A <= card i1 )
assume A is simplex-like ; :: thesis: card A <= card i1
then A in subset-closed_closure_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) by PRE_TOPC:def 2;
then consider B being set such that
A4: ( A c= B & B in the_subsets_with_limited_card ((i + 1), the topology of KX) ) by Th2;
( card A c= card B & card B c= card i1 ) by A4, Def2, CARD_1:11;
then card A c= card i1 by XBOOLE_1:1;
hence card A <= card i1 by NAT_1:39; :: thesis: verum

end;

hence Skeleton_of (KX,i) is finite-degree by MATROID0:def 7; :: thesis: verum