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 2;
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:11;
then A6: card s <= card a by NAT_1:39;
( a is simplex-like & not KX is void ) by A5, PENCIL_1:def 4, PRE_TOPC:def 2;
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;