let V be RealLinearSpace; :: thesis:
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis:
let Sk be finite simplex-like Subset-Family of K; :: thesis:
let Ak be Simplex of K; :: thesis:
set B = center_of_mass V;
assume that
A1: ( Sk is c=-linear & Sk is with_non-empty_elements ) and
A2: card Sk = card (union Sk) and
A3: union Sk c= Ak and
A4: card Ak = (card Sk) + 1 ; :: thesis:
card (Ak \ (union Sk)) = ((card Sk) + 1) - (card Sk) by A2, A3, A4, CARD_2:44
.= 1 ;
then consider v being object such that
A5: Ak \ (union Sk) = {v} by CARD_2:42;
reconsider Ak1 = @ Ak as finite affinely-independent Subset of V ;
set C = Complex_of {Ak1};
reconsider c = card Ak as ExtReal ;
A6: degree (Complex_of {Ak1}) = c - 1 by SIMPLEX0:26
.= (card Ak) + (- 1) by XXREAL_3:def 2
.= card Sk by A4 ;
reconsider Sk1 = @ Sk as c=-linear finite finite-membered Subset-Family of V by A1;
set XX = { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W } ;
set YY = { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ Ak) ) } ;
[#] K = the carrier of V by SIMPLEX0:def 10;
then |.K.| c= [#] K ;
then A7: subdivision ((center_of_mass V),K) = BCS K by Def5;
A8: Complex_of {Ak1} is SubSimplicialComplex of K by Th3;
then the topology of (Complex_of {Ak1}) c= the topology of K by SIMPLEX0:def 13;
then A9: |.(Complex_of {Ak1}).| c= |.K.| by Th4;
A10: [#] (Complex_of {Ak1}) = [#] V ;
then A11: degree (Complex_of {Ak1}) = degree (BCS (Complex_of {Ak1})) by A9, Th31;
subdivision ((center_of_mass V),(Complex_of {Ak1})) = BCS (Complex_of {Ak1}) by A9, A10, Def5;
then BCS (Complex_of {Ak1}) is SubSimplicialComplex of BCS K by A7, A8, SIMPLEX0:58;
then A12: degree (BCS (Complex_of {Ak1})) <= degree (BCS K) by SIMPLEX0:32;
A13: { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W } c= { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ Ak) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W } ; :: thesis:
then consider W being Simplex of card Sk, BCS (Complex_of {Ak1}) such that
A14: ( x = W & (center_of_mass V) .: Sk1 c= W ) ;
W = @ W ;
then reconsider w = W as Simplex of (BCS K) by Th40;
card W = (degree (BCS (Complex_of {Ak1}))) + 1 by A6, A11, SIMPLEX0:def 18;
then A15: w is Simplex of card Sk, BCS K by A6, A11, A12, SIMPLEX0:def 18;
( conv (@ W) c= conv (@ Ak) & @ w = w ) by Th40;
hence x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ Ak) ) } by A14, A15; :: thesis:

end;

A16: [#] (subdivision ((center_of_mass V),(Complex_of {Ak1}))) = [#] (Complex_of {Ak1}) by SIMPLEX0:def 20;
A17: { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ Ak) ) } c= { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider c1 = card Sk as ExtReal ;
assume x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ Ak) ) } ; :: thesis:
then consider W being Simplex of card Sk, BCS K such that
A18: ( W = x & (center_of_mass V) .: Sk c= W ) and
A19: conv (@ W) c= conv (@ Ak) ;
reconsider w = @ W as Subset of (BCS (Complex_of {Ak1})) by A9, A16, Def5;
reconsider cW = card W as ExtReal ;
card W = c1 + 1 by A6, A11, A12, SIMPLEX0:def 18
.= (card Sk) + 1 by XXREAL_3:def 2 ;
then card Sk = (card W) + (- 1) ;
then A20: card Sk = cW - 1 by XXREAL_3:def 2;
w is simplex-like by A19, Th40;
then w is Simplex of card Sk, BCS (Complex_of {Ak1}) by A20, SIMPLEX0:48;
hence x in { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W } by A18; :: thesis:

end;

v in {v} by TARSKI:def 1;
then A21: ( v in Ak1 & not v in union Sk ) by A5, XBOOLE_0:def 5;
Ak = Ak \/ (union Sk) by A3, XBOOLE_1:12
.= {v} \/ (union Sk1) by A5, XBOOLE_1:39 ;
then { W where W is Simplex of card Sk, BCS (Complex_of {Ak1}) : (center_of_mass V) .: Sk c= W } = {(((center_of_mass V) .: Sk1) \/ ((center_of_mass V) .: {Ak}))} by A1, A2, A21, Th38;
hence { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ Ak) ) } = {(((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: {Ak}))} by A13, A17; :: thesis: