theorem Th42: :: SIMPLEX1:42

for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Sk being finite simplex-like Subset-Family of K
for Ak being Simplex of K st Sk is c=-linear & Sk is with_non-empty_elements & card Sk = card (union Sk) & union Sk c= Ak & card Ak = (card Sk) + 1 holds
{ 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}))}