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:38;
( (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:145;
then card A c= card (S /\ (dom P)) by CARD_2:3;
then A5: card A <= card (S /\ (dom P)) by NAT_1:40;
(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:18;
SP \/ {{} } = (S /\ (dom P)) \/ {{} } by XBOOLE_1:39;
then A6: ( card {{} } = 1 & card (S /\ (dom P)) <= card (SP \/ {{} }) ) by CARD_1:50, NAT_1:44, XBOOLE_1:7;
card (SP \/ {{} }) <= (card SP) + (card {{} }) by CARD_2:62;
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:8;
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:64;
then not SP is with_empty_element by SETFAM_1:def 9;
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 card uSP c= d1 by NAT_1:40;
then card SP c= d1 by A11, XBOOLE_1:1;
then card SP <= d1 by NAT_1:40;
then (card SP) + 1 <= d1 + 1 by XREAL_1:8;
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;