theorem Th37: :: SIMPLEX1:37

for V being RealLinearSpace
for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})