let X be set ; :: thesis:
let K be subset-closed SimplicialComplexStr of X; :: thesis:
let P be Function; :: thesis:
assume that
A1: dom P is with_non-empty_elements and
A2: for n being Nat st n <= degree K holds
ex S being Subset of K st
( S is simplex-like & card S = n + 1 & BOOL S c= dom P & P .: (BOOL S) is Subset of K & P | (BOOL S) is one-to-one ) ; :: thesis:
set PP = subdivision (P,K);
A3: degree (subdivision (P,K)) <= degree K by A1, Th52;
A4: for n being Nat st n <= degree K holds
ex S being Simplex of (subdivision (P,K)) st card S = n + 1

proof

let n be Nat; :: thesis:
A5: [#] K = [#] (subdivision (P,K)) by Def20;
assume n <= degree K ; :: thesis:
then consider A being Subset of K such that
A6: A is simplex-like and
A7: card A = n + 1 and
A8: BOOL A c= dom P and
A9: P .: (BOOL A) is Subset of K and
A10: P | (BOOL A) is one-to-one by A2;
A11: dom (P | (BOOL A)) = BOOL A by A8, RELAT_1:62;
not A is empty by A7;
then consider S being Subset-Family of A such that
A12: ( S is with_non-empty_elements & S is c=-linear ) and
A in S and
A13: card A = card S and
for Z being set st Z in S & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in S ) by Th12;
bool A c= bool the carrier of K by ZFMISC_1:67;
then reconsider SS = S as Subset-Family of K by XBOOLE_1:1;
A14: S c= BOOL A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in S ; :: thesis:
then x in (bool A) \ {{}} by A12, ZFMISC_1:56;
hence x in BOOL A by ORDERS_1:def 3; :: thesis:

end;

then P .: S c= P .: (BOOL A) by RELAT_1:123;
then reconsider PS = P .: SS as Subset of (subdivision (P,K)) by A5, A9, XBOOLE_1:1;
A15: A in the_family_of K by A6;
SS is simplex-like

proof

let B be Subset of K; :: according to TOPS_2:def 1 :: thesis:
assume B in SS ; :: thesis:
then B in the_family_of K by A15, CLASSES1:def 1;
hence B is simplex-like ; :: thesis:

end;

then SS is c=-linear finite simplex-like Subset-Family of K by A7, A12, A13;
then reconsider PS = PS as Simplex of (subdivision (P,K)) by Def20;
P .: S = (P | (BOOL A)) .: S by A14, RELAT_1:129;
then card PS = n + 1 by A7, A10, A11, A13, A14, COMBGRAS:4;
hence ex S being Simplex of (subdivision (P,K)) st card S = n + 1 ; :: thesis:

end;

per cases ;

suppose A16: K is empty-membered ; :: thesis:

A17: degree (subdivision (P,K)) >= - 1 by Th23;
degree K = - 1 by A16, Th22;
hence degree (subdivision (P,K)) = degree K by A3, A17, XXREAL_0:1; :: thesis:

end;

suppose A18: ( K is with_non-empty_element & K is finite-degree ) ; :: thesis:

then reconsider d = degree K, dPP = degree (subdivision (P,K)) as Integer ;
A19: - 1 <= d by Th23;
d <> - 1 by A18, Th22;
then - 1 < d by A19, XXREAL_0:1;
then 0 <= d by INT_1:8;
then reconsider d = d as Element of NAT by INT_1:3;
ex S being Simplex of (subdivision (P,K)) st card S = d + 1 by A4;
then dPP + 1 >= d + 1 by A18, Def12;
then dPP >= d by XREAL_1:6;
hence degree (subdivision (P,K)) = degree K by A3, XXREAL_0:1; :: thesis:

end;

suppose ( not K is void & not K is finite-degree ) ; :: thesis:

then A20: degree K = +infty by Def12;
not subdivision (P,K) is finite-degree

proof

assume A21: subdivision (P,K) is finite-degree ; :: thesis:
then reconsider d = (degree (subdivision (P,K))) + 1 as Nat by TARSKI:1;
consider S being Subset of (subdivision (P,K)) such that
A22: S is simplex-like and
A23: card S = d by A21, Def12;
reconsider S = S as finite Subset of (subdivision (P,K)) by A22;
ex S1 being Simplex of (subdivision (P,K)) st card S1 = (card S) + 1 by A4, A20, XXREAL_0:3;
then d + 1 <= d by A21, A23, Def12;
hence contradiction by NAT_1:13; :: thesis:

end;

hence degree (subdivision (P,K)) = degree K by A20, Def12; :: thesis:

end;

end;