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

now :: thesis: for A being finite Subset of (Complex_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX))) st A is open holds
card A <= i1

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

end;

hence Skeleton_of (KX,i) is finite-degree ; :: thesis: verum