theorem Th36: :: SIMPLEX1:36

for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )