let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

let Sk be finite simplex-like Subset-Family of K; :: thesis: ( Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) implies card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 )

set B = center_of_mass V;

assume that

A1: ( Sk is c=-linear & Sk is with_non-empty_elements ) and

A2: (card Sk) + 1 = card (union Sk) ; :: thesis: card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

not Sk is empty by A2, ZFMISC_1:2;

then union Sk in Sk by A1, SIMPLEX0:9;

then reconsider U = union Sk as Simplex of K by TOPS_2:def 1;

reconsider Sk1 = @ Sk as c=-linear finite finite-membered Subset-Family of V by A1;

reconsider c = card U as ExtReal ;

@ U = union Sk1 ;

then reconsider U1 = union Sk1 as finite affinely-independent Subset of V ;

set C = Complex_of {U1};

A3: degree (Complex_of {U1}) = c - 1 by SIMPLEX0:26

.= (card U) + (- 1) by XXREAL_3:def 2

.= card Sk by A2 ;

set YY = { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } ;

[#] K = the carrier of V by SIMPLEX0:def 10;

then |.K.| c= [#] K ;

then A4: subdivision ((center_of_mass V),K) = BCS K by Def5;

set XX = { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } ;

A5: @ U = U1 ;

then A6: Complex_of {U1} is SubSimplicialComplex of K by Th3;

then the topology of (Complex_of {U1}) c= the topology of K by SIMPLEX0:def 13;

then A7: |.(Complex_of {U1}).| c= |.K.| by Th4;

A8: [#] (Complex_of {U1}) = [#] V ;

then A9: degree (Complex_of {U1}) = degree (BCS (Complex_of {U1})) by A7, Th31;

subdivision ((center_of_mass V),(Complex_of {U1})) = BCS (Complex_of {U1}) by A7, A8, Def5;

then BCS (Complex_of {U1}) is SubSimplicialComplex of BCS K by A4, A6, SIMPLEX0:58;

then A10: degree (BCS (Complex_of {U1})) <= degree (BCS K) by SIMPLEX0:32;

A11: { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (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 (@ (union Sk)) ) }

A15: { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } c= { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }

hence card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 by A11, A15, XBOOLE_0:def 10; :: thesis: verum

for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds

card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

let Sk be finite simplex-like Subset-Family of K; :: thesis: ( Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) implies card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 )

set B = center_of_mass V;

assume that

A1: ( Sk is c=-linear & Sk is with_non-empty_elements ) and

A2: (card Sk) + 1 = card (union Sk) ; :: thesis: card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2

not Sk is empty by A2, ZFMISC_1:2;

then union Sk in Sk by A1, SIMPLEX0:9;

then reconsider U = union Sk as Simplex of K by TOPS_2:def 1;

reconsider Sk1 = @ Sk as c=-linear finite finite-membered Subset-Family of V by A1;

reconsider c = card U as ExtReal ;

@ U = union Sk1 ;

then reconsider U1 = union Sk1 as finite affinely-independent Subset of V ;

set C = Complex_of {U1};

A3: degree (Complex_of {U1}) = c - 1 by SIMPLEX0:26

.= (card U) + (- 1) by XXREAL_3:def 2

.= card Sk by A2 ;

set YY = { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } ;

[#] K = the carrier of V by SIMPLEX0:def 10;

then |.K.| c= [#] K ;

then A4: subdivision ((center_of_mass V),K) = BCS K by Def5;

set XX = { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } ;

A5: @ U = U1 ;

then A6: Complex_of {U1} is SubSimplicialComplex of K by Th3;

then the topology of (Complex_of {U1}) c= the topology of K by SIMPLEX0:def 13;

then A7: |.(Complex_of {U1}).| c= |.K.| by Th4;

A8: [#] (Complex_of {U1}) = [#] V ;

then A9: degree (Complex_of {U1}) = degree (BCS (Complex_of {U1})) by A7, Th31;

subdivision ((center_of_mass V),(Complex_of {U1})) = BCS (Complex_of {U1}) by A7, A8, Def5;

then BCS (Complex_of {U1}) is SubSimplicialComplex of BCS K by A4, A6, SIMPLEX0:58;

then A10: degree (BCS (Complex_of {U1})) <= degree (BCS K) by SIMPLEX0:32;

A11: { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (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 (@ (union Sk)) ) }

proof

A14:
[#] (subdivision ((center_of_mass V),(Complex_of {U1}))) = [#] (Complex_of {U1})
by SIMPLEX0:def 20;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } or x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } )

assume x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } ; :: thesis: x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }

then consider W being Simplex of card Sk, BCS (Complex_of {U1}) such that

A12: ( x = W & (center_of_mass V) .: Sk1 c= W ) ;

W = @ W ;

then reconsider w = W as Simplex of (BCS K) by A5, Th40;

card W = (degree (BCS (Complex_of {U1}))) + 1 by A3, A9, SIMPLEX0:def 18;

then A13: w is Simplex of card Sk, BCS K by A3, A9, A10, SIMPLEX0:def 18;

( conv (@ W) c= conv (@ U) & @ 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 (@ (union Sk)) ) } by A12, A13; :: thesis: verum

end;assume x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } ; :: thesis: x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }

then consider W being Simplex of card Sk, BCS (Complex_of {U1}) such that

A12: ( x = W & (center_of_mass V) .: Sk1 c= W ) ;

W = @ W ;

then reconsider w = W as Simplex of (BCS K) by A5, Th40;

card W = (degree (BCS (Complex_of {U1}))) + 1 by A3, A9, SIMPLEX0:def 18;

then A13: w is Simplex of card Sk, BCS K by A3, A9, A10, SIMPLEX0:def 18;

( conv (@ W) c= conv (@ U) & @ 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 (@ (union Sk)) ) } by A12, A13; :: thesis: verum

A15: { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } c= { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }

proof

card { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } = 2
by A1, A2, Th39;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } or x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } )

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 (@ (union Sk)) ) } ; :: thesis: x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }

then consider W being Simplex of card Sk, BCS K such that

A16: ( W = x & (center_of_mass V) .: Sk c= W ) and

A17: conv (@ W) c= conv (@ U) ;

reconsider w = @ W as Subset of (BCS (Complex_of {U1})) by A7, A14, Def5;

reconsider cW = card W as ExtReal ;

card W = c1 + 1 by A3, A9, A10, SIMPLEX0:def 18

.= (card Sk) + 1 by XXREAL_3:def 2 ;

then card Sk = (card W) + (- 1) ;

then A18: card Sk = cW - 1 by XXREAL_3:def 2;

w is simplex-like by A17, Th40;

then w is Simplex of card Sk, BCS (Complex_of {U1}) by A18, SIMPLEX0:48;

hence x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } by A16; :: thesis: verum

end;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 (@ (union Sk)) ) } ; :: thesis: x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }

then consider W being Simplex of card Sk, BCS K such that

A16: ( W = x & (center_of_mass V) .: Sk c= W ) and

A17: conv (@ W) c= conv (@ U) ;

reconsider w = @ W as Subset of (BCS (Complex_of {U1})) by A7, A14, Def5;

reconsider cW = card W as ExtReal ;

card W = c1 + 1 by A3, A9, A10, SIMPLEX0:def 18

.= (card Sk) + 1 by XXREAL_3:def 2 ;

then card Sk = (card W) + (- 1) ;

then A18: card Sk = cW - 1 by XXREAL_3:def 2;

w is simplex-like by A17, Th40;

then w is Simplex of card Sk, BCS (Complex_of {U1}) by A18, SIMPLEX0:48;

hence x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } by A16; :: thesis: verum

hence card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 by A11, A15, XBOOLE_0:def 10; :: thesis: verum