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 : ( () .: 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 : ( () .: 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 : ( () .: 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 : ( () .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
not Sk is empty by ;
then union Sk in Sk by ;
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 () = 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 : ( () .: 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 ((),K) = BCS K by Def5;
set XX = { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } ;
A5: @ U = U1 ;
then A6: Complex_of {U1} is SubSimplicialComplex of K by Th3;
then the topology of () c= the topology of K by SIMPLEX0:def 13;
then A7: |.().| c= |.K.| by Th4;
A8: [#] () = [#] V ;
then A9: degree () = degree (BCS ()) by ;
subdivision ((),()) = BCS () by A7, A8, Def5;
then BCS () is SubSimplicialComplex of BCS K by ;
then A10: degree (BCS ()) <= degree (BCS K) by SIMPLEX0:32;
A11: { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } c= { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } or x in { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } )
assume x in { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } ; :: thesis: x in { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
then consider W being Simplex of card Sk, BCS () such that
A12: ( x = W & () .: Sk1 c= W ) ;
W = @ W ;
then reconsider w = W as Simplex of (BCS K) by ;
card W = (degree (BCS ())) + 1 by ;
then A13: w is Simplex of card Sk, BCS K by ;
( conv (@ W) c= conv (@ U) & @ w = w ) by Th40;
hence x in { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } by ; :: thesis: verum
end;
A14: [#] (subdivision ((),())) = [#] () by SIMPLEX0:def 20;
A15: { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } c= { W where W is Simplex of card Sk, BCS () : () .: Sk c= W }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } or x in { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } )
reconsider c1 = card Sk as ExtReal ;
assume x in { W where W is Simplex of card Sk, BCS K : ( () .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } ; :: thesis: x in { W where W is Simplex of card Sk, BCS () : () .: Sk c= W }
then consider W being Simplex of card Sk, BCS K such that
A16: ( W = x & () .: Sk c= W ) and
A17: conv (@ W) c= conv (@ U) ;
reconsider w = @ W as Subset of (BCS ()) by ;
reconsider cW = card W as ExtReal ;
card W = c1 + 1 by
.= (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 ;
then w is Simplex of card Sk, BCS () by ;
hence x in { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } by A16; :: thesis: verum
end;
card { W where W is Simplex of card Sk, BCS () : () .: Sk c= W } = 2 by A1, A2, Th39;
hence card { S1 where S1 is Simplex of card Sk, BCS K : ( () .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 by ; :: thesis: verum