theorem Th35: :: SIMPLEX1:35

for n being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for Bf being finite Subset of V
for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )