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

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