for n being Nat
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Af being finite Subset of V
for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds
( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st
( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )