let n be Nat; :: thesis:
let V be RealLinearSpace; :: thesis:
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis:
let Af be finite Subset of V; :: thesis:
let Sk be finite simplex-like Subset-Family of K; :: thesis:
set B = center_of_mass V;
set BK = BCS K;
assume that
A1: Sk is with_non-empty_elements and
A2: (card Sk) + n <= degree K ; :: thesis:
reconsider nc = n + (card Sk) as ExtReal ;
A3: (nc + 1) - 1 = nc by XXREAL_3:22;
A4: [#] K = the carrier of V by SIMPLEX0:def 10;
then A5: |.K.| c= [#] K ;
then A6: subdivision ((center_of_mass V),K) = BCS K by Def5;
A7: nc <= degree (BCS K) by A2, A5, Th31;

hereby :: thesis:

assume that
A8: Af is Simplex of n + (card Sk), BCS K and
A9: (center_of_mass V) .: Sk c= Af ; :: thesis:
consider T being c=-linear finite simplex-like Subset-Family of K such that
A10: Af = (center_of_mass V) .: T by A6, A8, SIMPLEX0:def 20;
( union T is empty or union T in T ) by SIMPLEX0:9, ZFMISC_1:2;
then A11: union T is simplex-like by TOPS_2:def 1;
then @ (union T) is affinely-independent ;
then reconsider UT = union T as finite affinely-independent Subset of V ;
UT = union (@ T) ;
then conv Af c= conv UT by A10, CONVEX1:30, RLAFFIN2:17;
then reconsider s1 = Af as Simplex of (BCS (Complex_of {UT})) by A8, A11, Th40;
card Af = nc + 1 by A7, A8, SIMPLEX0:def 18;
then A12: s1 is Simplex of n + (card Sk), BCS (Complex_of {UT}) by A3, SIMPLEX0:48;
set C = Complex_of {UT};
reconsider cT = card UT as ExtReal ;
|.(Complex_of {UT}).| c= [#] (Complex_of {UT}) ;
then A13: degree (Complex_of {UT}) = degree (BCS (Complex_of {UT})) by Th31;
( degree (Complex_of {UT}) = cT - 1 & card s1 <= (degree (BCS (Complex_of {UT}))) + 1 ) by SIMPLEX0:24, SIMPLEX0:26;
then card s1 <= card UT by A13, XXREAL_3:22;
then nc + 1 <= card UT by A7, A8, SIMPLEX0:def 18;
then A14: ((card Sk) + n) + 1 <= card UT by XXREAL_3:def 2;
( the_family_of K is subset-closed & UT in the topology of K ) by A11;
then A15: bool UT c= the topology of K by SIMPLEX0:1;
union (@ Sk) c= union T by A1, A5, A8, A9, A10, Th34, ZFMISC_1:77;
then consider R being finite Subset-Family of V such that
A16: ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 ) and
A17: union R c= UT and
A18: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) by A1, A9, A12, A14, Th35;
reconsider R = R as Subset-Family of K by A4;
( R c= bool (union R) & bool (union R) c= bool UT ) by A17, SIMPLEX0:1, ZFMISC_1:82;
then R c= bool UT ;
then R c= the topology of K by A15;
then reconsider R = R as finite simplex-like Subset-Family of K by SIMPLEX0:14;
take R = R; :: thesis:
thus ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) ) by A16, A18; :: thesis:

end;

given T being finite simplex-like Subset-Family of K such that A19: T misses Sk and
A20: ( T \/ Sk is c=-linear & T \/ Sk is with_non-empty_elements ) and
A21: card T = n + 1 and
A22: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) ; :: thesis:
set ST = Sk \/ T;
[#] K = [#] (BCS K) by A6, SIMPLEX0:def 20;
then reconsider BST = (center_of_mass V) .: (Sk \/ T) as Subset of (BCS K) by SIMPLEX0:def 10;
A23: Sk \/ T is simplex-like by TOPS_2:13;
then reconsider BST = BST as Simplex of (BCS K) by A6, A20, SIMPLEX0:def 20;
card (Sk \/ T) = (card Sk) + (card T) by A19, CARD_2:40;
then card BST = ((card Sk) + n) + 1 by A20, A21, A23, Th33;
then ( ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) = (center_of_mass V) .: (Sk \/ T) & card BST = nc + 1 ) by RELAT_1:120, XXREAL_3:def 2;
hence ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) by A3, A22, SIMPLEX0:48, XBOOLE_1:7; :: thesis: