let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for i being dim-like number 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: for i being dim-like number st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i
let i be dim-like number ; :: 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 KX is with_non-empty_element ) ;

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: KX is with_non-empty_element ; :: thesis: ( not Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) or degree KX <= i )

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

A4: now :: thesis: for S being finite Subset of KX st S is simplex-like holds
card S <= i1

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;
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:11;
then A6: card S c= card (Segm i1) ;
card S = card (Segm (card S)) ;
hence card S <= i1 by A6, NAT_1:40; :: thesis: verum

end;

for x being set st x in the topology of KX holds
x is finite by A3;
then the_family_of KX is finite-membered ;
then KX is finite-membered ;
hence degree KX <= i by A2, A4, Th25; :: thesis: verum

end;

end;