let X be set ; :: thesis: for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) holds
degree KX <= i
let i be Integer; :: thesis: for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) holds
degree KX <= i
let KX be SimplicialComplexStr of X; :: thesis: ( - 1 <= i & Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) implies degree KX <= i )
assume A1: - 1 <= i ; :: thesis: ( not Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) or degree KX <= i )

per cases ( KX is empty-membered or not KX is empty-membered ) ;

suppose KX is empty-membered ; :: thesis: ( not Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) or degree KX <= i )

hence ( not Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) or degree KX <= i ) by A1, Th22; :: thesis: verum

end;

suppose A2: not KX is empty-membered ; :: thesis: ( not Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) or degree KX <= i )

(- 1) + 1 <= i + 1 by A1, XREAL_1:8;
then reconsider i1 = i + 1 as Element of NAT by INT_1:16;
assume A3: Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) ; :: thesis: degree KX <= i

A4: now

let S be finite Subset of KX; :: thesis: ( S is simplex-like implies card S <= i1 )
assume S is simplex-like ; :: thesis: card S <= i1
then S in subset-closed_closure_of (the_subsets_with_limited_card i1,the topology of KX) by A3, PRE_TOPC:def 5;
then consider y being set such that
A5: ( S c= y & y in the_subsets_with_limited_card i1,the topology of KX ) by Th2;
( card S c= card y & card y c= card i1 ) by A5, Def2, CARD_1:27;
then A6: card S c= card i1 by XBOOLE_1:1;
card S = card (card S) ;
hence card S <= i1 by A6, NAT_1:41; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in the topology of KX implies x is finite )
assume x in the topology of KX ; :: thesis: x is finite
then consider y being set such that
A7: ( x c= y & y in the_subsets_with_limited_card i1,the topology of KX ) by A3, Th2;
( card x c= card y & card y c= card i1 ) by A7, Def2, CARD_1:27;
hence x is finite ; :: thesis: verum

end;

then the_family_of KX is finite-membered by MATROID0:def 5;
then KX is finite-membered by MATROID0:def 6;
hence degree KX <= i by A2, A4, Th25; :: thesis: verum

end;

end;