for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Aff being finite affinely-independent Subset of V
for B being Subset of V st Aff is Simplex of K holds
( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )