let k be Nat; :: thesis: for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff
let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff
let Aff be finite affinely-independent Subset of V; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff
let F be Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) implies ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff )
set XX = { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } ;
assume for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ; :: thesis: ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff
then ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1 by Th46;
then not { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } is empty ;
then consider x being object such that
A1: x in { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } ;
ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st
( x = S & F .: S = Aff ) by A1;
hence ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff ; :: thesis: verum