for V being RealLinearSpace
for Kv being non void SimplicialComplex of V
for S being Simplex of (BCS Kv)
for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds
for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )