let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
let KX be SimplicialComplexStr of X; :: thesis: for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
let P be Function; :: thesis: degree (subdivision (P,KX)) <= (degree KX) + 1
set PP = subdivision (P,KX);

per cases ( KX is void or ( not KX is void & not KX is finite-degree ) or ( not KX is void & KX is finite-degree ) ) ;

suppose KX is void ; :: thesis: degree (subdivision (P,KX)) <= (degree KX) + 1

then ( KX is empty-membered & degree (subdivision (P,KX)) = - 1 ) by Th22;
hence degree (subdivision (P,KX)) <= (degree KX) + 1 ; :: thesis: verum

end;

suppose A1: ( not KX is void & not KX is finite-degree ) ; :: thesis: degree (subdivision (P,KX)) <= (degree KX) + 1

A2: ( degree (subdivision (P,KX)) <= +infty & (degree KX) + 0 <= (degree KX) + 1 ) by XXREAL_0:3, XXREAL_3:36;
( (degree KX) + 0 = degree KX & degree KX = +infty ) by A1, Def12, XXREAL_3:4;
hence degree (subdivision (P,KX)) <= (degree KX) + 1 by A2, XXREAL_0:2; :: thesis: verum

end;

suppose A3: ( not KX is void & KX is finite-degree ) ; :: thesis: degree (subdivision (P,KX)) <= (degree KX) + 1

then reconsider d = degree KX as Integer ;
reconsider d1 = d + 1 as Nat by A3;
for A being finite Subset of (subdivision (P,KX)) st A is simplex-like holds
card A <= (d + 1) + 1

proof

let A be finite Subset of (subdivision (P,KX)); :: thesis: ( A is simplex-like implies card A <= (d + 1) + 1 )
assume A is simplex-like ; :: thesis: card A <= (d + 1) + 1
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: A = P .: S by Def20;
set Sd = S /\ (dom P);
A = P .: (S /\ (dom P)) by A4, RELAT_1:112;
then Segm (card A) c= Segm (card (S /\ (dom P))) by CARD_1:67;
then A5: card A <= card (S /\ (dom P)) by NAT_1:39;
(S /\ (dom P)) \ {{}} c= S by XBOOLE_1:18, XBOOLE_1:36;
then reconsider SP = (S /\ (dom P)) \ {{}} as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:11;
SP \/ {{}} = (S /\ (dom P)) \/ {{}} by XBOOLE_1:39;
then A6: ( card {{}} = 1 & card (S /\ (dom P)) <= card (SP \/ {{}}) ) by CARD_1:30, NAT_1:43, XBOOLE_1:7;
card (SP \/ {{}}) <= (card SP) + (card {{}}) by CARD_2:43;
then A7: card (S /\ (dom P)) <= (card SP) + 1 by A6, XXREAL_0:2;

per cases ( SP is empty or not SP is empty ) ;

suppose A8: SP is empty ; :: thesis: card A <= (d + 1) + 1

0 + 1 <= d1 + 1 by XREAL_1:6;
then card (S /\ (dom P)) <= d1 + 1 by A6, A8, XXREAL_0:2;
hence card A <= (d + 1) + 1 by A5, XXREAL_0:2; :: thesis: verum

end;

suppose A9: not SP is empty ; :: thesis: card A <= (d + 1) + 1

reconsider uSP = union SP as Subset of KX ;
union SP in SP by A9, Th9;
then A10: uSP is simplex-like by TOPS_2:def 1;
not {} in SP by ZFMISC_1:56;
then SP is with_non-empty_elements ;
then A11: card SP c= card (union SP) by Th10;
reconsider uSP = uSP as finite Subset of KX by A3;
card uSP <= d1 by A3, A10, Th25;
then Segm (card uSP) c= Segm d1 by NAT_1:39;
then Segm (card SP) c= Segm d1 by A11;
then card SP <= d1 by NAT_1:39;
then (card SP) + 1 <= d1 + 1 by XREAL_1:6;
then card (S /\ (dom P)) <= d1 + 1 by A7, XXREAL_0:2;
hence card A <= (d + 1) + 1 by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence degree (subdivision (P,KX)) <= (degree KX) + 1 by Th25; :: thesis: verum

end;

end;