theorem Th45: :: SIMPLEX1:45

for X being set
for n, k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )