let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for i being dim-like number st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
let KX be SimplicialComplexStr of X; :: thesis: for i being dim-like number st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
let i be dim-like number ; :: thesis: ( - 1 <= i implies degree (Skeleton_of (KX,i)) <= i )
set swlc = the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX);
set S = Skeleton_of (KX,i);
assume A1: - 1 <= i ; :: thesis: degree (Skeleton_of (KX,i)) <= i
reconsider i1 = i + 1 as Element of NAT by INT_1:3;

now :: thesis: for A being finite Subset of (Skeleton_of (KX,i)) st A is simplex-like holds
card A <= i + 1

let A be finite Subset of (Skeleton_of (KX,i)); :: thesis: ( A is simplex-like implies card A <= i + 1 )
assume A is simplex-like ; :: thesis: card A <= i + 1
then A in the topology of (Skeleton_of (KX,i)) ;
then consider x being set such that
A2: ( A c= x & x in the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX) ) by Th2;
( card x c= card (Segm (i + 1)) & card A c= card x ) by A2, Def2, CARD_1:11;
then A3: card A c= card (Segm i1) ;
card (Segm (card A)) = card A ;
hence card A <= i + 1 by A3, NAT_1:40; :: thesis: verum

end;

hence degree (Skeleton_of (KX,i)) <= i by A1, Th25; :: thesis: verum