let X be set ; :: thesis:
let KX be SimplicialComplexStr of X; :: thesis:
let i be dim-like number ; :: 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)) ;
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: a in the topology of KX by A3, Def2;
reconsider a = a as finite Subset of KX by A3;
Segm (card s) c= Segm (card a) by A2, CARD_1:11;
then A5: card s <= card a by NAT_1:39;
( a is simplex-like & not KX is void ) by A4, PENCIL_1:def 4;
then card a <= d + 1 by Th25;
hence card s <= d + 1 by A5, XXREAL_0:2; :: thesis:

end;

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

end;

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

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

end;

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

end;

end;