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

now

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)) by PRE_TOPC:def 2;
then consider x being set such that
A2: ( A c= x & x in the_subsets_with_limited_card ((i + 1), the topology of KX) ) by Th2;
( card x c= card (i + 1) & card A c= card x ) by A2, Def2, CARD_1:11;
then A3: card A c= card i1 by XBOOLE_1:1;
card (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