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 st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K
for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds
( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds
for S being Simplex of n - 1, BCS K
for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds
( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )