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 5;
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:27;
then card A c= card i1 by XBOOLE_1:1;
hence card A <= card i1 by NAT_1:40; :: thesis: verum

end;

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