let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
let P be Function; :: thesis: ( dom P is with_non-empty_elements implies degree (subdivision (P,KX)) <= degree KX )
assume A1: dom P is with_non-empty_elements ; :: thesis: degree (subdivision (P,KX)) <= degree KX
set PP = subdivision (P,KX);

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

suppose A2: not KX is finite-degree ; :: thesis: degree (subdivision (P,KX)) <= degree KX

not KX is void

proof

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

end;

then degree KX = +infty by A2, Def12;
hence degree (subdivision (P,KX)) <= degree KX by XXREAL_0:3; :: thesis: verum

end;

suppose A3: KX is finite-degree ; :: thesis: degree (subdivision (P,KX)) <= degree KX

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

proof

let A be finite Subset of (subdivision (P,KX)); :: thesis: ( A is simplex-like implies card A <= d + 1 )
assume A is simplex-like ; :: thesis: card A <= d + 1
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: A = P .: S by Def20;
A5: A = P .: (S /\ (dom P)) by A4, RELAT_1:112;

per cases ( S /\ (dom P) is empty or not S /\ (dom P) is empty ) ;

suppose S /\ (dom P) is empty ; :: thesis: card A <= d + 1

then ( 0 <= d1 & A = {} ) by A5;
hence card A <= d + 1 ; :: thesis: verum

end;

suppose A6: not S /\ (dom P) is empty ; :: thesis: card A <= d + 1

reconsider uSP = union (S /\ (dom P)) as Subset of KX ;
A7: S /\ (dom P) c= S by XBOOLE_1:17;
then union (S /\ (dom P)) in S /\ (dom P) by A6, Th9;
then union (S /\ (dom P)) in S by XBOOLE_0:def 4;
then A8: uSP is simplex-like by TOPS_2:def 1;
then A9: uSP in the topology of KX ;
the_family_of KX is finite-membered by A3, MATROID0:def 6;
then reconsider uSP = uSP as finite Subset of KX by A9;
not KX is void by A9, PENCIL_1:def 4;
then card uSP <= d + 1 by A8, Th25;
then A10: Segm (card uSP) c= Segm d1 by NAT_1:39;
card (S /\ (dom P)) c= card (union (S /\ (dom P))) by A1, A7, Th10;
then A11: card (S /\ (dom P)) c= d1 by A10;
card A c= card (S /\ (dom P)) by A5, CARD_1:67;
then Segm (card A) c= Segm d1 by A11;
hence card A <= d + 1 by NAT_1:39; :: thesis: verum

end;

end;

end;

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

end;

end;