let X be set ; :: thesis:
let i be Integer; :: thesis:
let KX be SimplicialComplexStr of X; :: thesis:
set S = Skeleton_of KX,i;

suppose ( KX is void or Skeleton_of KX,i is void ) ; :: thesis:

then ( KX is empty-membered or Skeleton_of KX,i is empty-membered ) ;
then degree (Skeleton_of KX,i) = - 1 by Th22;
hence degree (Skeleton_of KX,i) <= degree KX by Th23; :: thesis:

end;

suppose A1: ( not KX is void & KX is finite-degree & not Skeleton_of KX,i is void ) ; :: thesis:

then reconsider d = degree KX as Integer ;

let s be finite Subset of (Skeleton_of KX,i); :: thesis:
assume s is simplex-like ; :: thesis:
then s in subset-closed_closure_of (the_subsets_with_limited_card (i + 1),the topology of KX) by PRE_TOPC:def 5;
then consider a being set such that
A2: s c= a and
A3: a in the_subsets_with_limited_card (i + 1),the topology of KX by Th2;
A4: card a c= card (i + 1) by A3, Def2;
A5: a in the topology of KX by A3, Def2;
reconsider a = a as finite Subset of KX by A3, A4;
card s c= card a by A2, CARD_1:27;
then A6: card s <= card a by NAT_1:40;
( a is simplex-like & not KX is void ) by A5, PENCIL_1:def 4, PRE_TOPC:def 5;
then card a <= d + 1 by Th25;
hence card s <= d + 1 by A6, XXREAL_0:2; :: thesis:

end;

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

end;

suppose A7: not KX is finite-degree ; :: thesis:

assume KX is void ; :: thesis:
then KX is empty-membered ;
hence contradiction by A7; :: thesis:

end;

then degree KX = +infty by A7, Def12;
hence degree (Skeleton_of KX,i) <= degree KX by XXREAL_0:3; :: thesis:

end;

end;