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 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

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 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

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 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

reconsider O = 1 as ExtReal ;
reconsider Z = 0 as ExtReal ;
defpred S1[ Nat] means for A being finite affinely-independent Subset of V st card A = \$1 holds
for F being Function of (Vertices (BCS (k,()))),A st ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; :: thesis: S1[m + 1]
let A be finite affinely-independent Subset of V; :: thesis: ( card A = m + 1 implies for F being Function of (Vertices (BCS (k,()))),A st ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1 )

assume A3: card A = m + 1 ; :: thesis: for F being Function of (Vertices (BCS (k,()))),A st ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1

not A is empty by A3;
then consider a being object such that
A4: a in A ;
reconsider a = a as Element of V by A4;
A5: card (A \ {a}) = m by ;
reconsider Aa = A \ {a} as finite affinely-independent Subset of V by ;
set CAa = Complex_of {Aa};
the topology of () = bool Aa by SIMPLEX0:4;
then A6: Vertices () = union (bool Aa) by SIMPLEX0:16
.= Aa by ZFMISC_1:81 ;
A7: ( [#] () = [#] V & |.().| c= [#] V ) ;
then A8: Vertices () c= Vertices (BCS (k,())) by Th24;
set CA = Complex_of {A};
let F be Function of (Vertices (BCS (k,()))),A; :: thesis: ( ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1 )

assume A9: for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1
set XX = { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } ;
A10: { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } c= the topology of (BCS (k,()))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } or x in the topology of (BCS (k,())) )
assume x in { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } ; :: thesis: x in the topology of (BCS (k,()))
then ex S being Simplex of (card A) - 1, BCS (k,()) st
( S = x & A = F .: S ) ;
hence x in the topology of (BCS (k,())) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider XX = { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } as Subset-Family of (BCS (k,())) by XBOOLE_1:1;
reconsider XX = XX as simplex-like Subset-Family of (BCS (k,())) by ;
A11: ( [#] () = [#] V & |.().| c= [#] V ) ;
A12: A \ {a} c= A by XBOOLE_1:36;
for x being set st x in {Aa} holds
ex y being set st
( y in {A} & x c= y )
proof
let x be set ; :: thesis: ( x in {Aa} implies ex y being set st
( y in {A} & x c= y ) )

assume A13: x in {Aa} ; :: thesis: ex y being set st
( y in {A} & x c= y )

take A ; :: thesis: ( A in {A} & x c= A )
thus ( A in {A} & x c= A ) by ; :: thesis: verum
end;
then {Aa} is_finer_than {A} ;
then Complex_of {Aa} is SubSimplicialComplex of Complex_of {A} by SIMPLEX0:30;
then A14: BCS (k,()) is SubSimplicialComplex of BCS (k,()) by ;
then A15: Vertices (BCS (k,())) c= Vertices (BCS (k,())) by SIMPLEX0:31;
A16: the topology of () = bool A by SIMPLEX0:4;
then A17: Vertices () = union (bool A) by SIMPLEX0:16
.= A by ZFMISC_1:81 ;
A18: dom F = Vertices (BCS (k,())) by ;
per cases ( m = 0 or m > 0 ) ;
suppose A19: m = 0 ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1
A20: O - 1 = 0 by XXREAL_3:7;
then A21: degree () = 0 by ;
( k = 0 or k > 0 ) ;
then A22: BCS (k,()) = Complex_of {A} by ;
then A23: dom F = Vertices () by ;
take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * 0) + 1
A in bool A by ZFMISC_1:def 1;
then reconsider A1 = A as Simplex of () by ;
A24: A1 is Simplex of 0 , Complex_of {A} by ;
ex x being object st A = {x} by ;
then A25: A = {a} by ;
then conv A = A by RLAFFIN1:1;
then F . a in A by A4, A9, A17, A22;
then A26: F . a = a by ;
A27: XX c= {A}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX or x in {A} )
assume x in XX ; :: thesis: x in {A}
then consider S being Simplex of 0 , Complex_of {A} such that
A28: x = S and
F .: S = A by A3, A19, A22;
A29: S in the topology of () by PRE_TOPC:def 2;
card S = Z + 1 by
.= 1 by XXREAL_3:4 ;
then S = A by ;
hence x in {A} by ; :: thesis: verum
end;
F .: A = Im (F,a) by
.= A by ;
then A in XX by A3, A19, A24, A22;
then XX = {A} by ;
hence card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum
end;
suppose A30: m > 0 ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1
defpred S2[ object , object ] means ex D1, D2 being set st
( D1 = \$1 & D2 = \$2 & D1 c= D2 );
set XXA = { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
reconsider m1 = m - 1 as ExtReal ;
reconsider M = m as ExtReal ;
reconsider cA = card A as ExtReal ;
set YA = { S where S is Simplex of m, BCS (k,()) : Aa = F .: S } ;
A31: { S where S is Simplex of m, BCS (k,()) : Aa = F .: S } c= the topology of (BCS (k,()))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m, BCS (k,()) : Aa = F .: S } or x in the topology of (BCS (k,())) )
assume x in { S where S is Simplex of m, BCS (k,()) : Aa = F .: S } ; :: thesis: x in the topology of (BCS (k,()))
then ex S being Simplex of m, BCS (k,()) st
( S = x & Aa = F .: S ) ;
hence x in the topology of (BCS (k,())) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider YA = { S where S is Simplex of m, BCS (k,()) : Aa = F .: S } as Subset-Family of (BCS (k,())) by XBOOLE_1:1;
reconsider YA = YA as simplex-like Subset-Family of (BCS (k,())) by ;
defpred S3[ object , object ] means ex D1, D2 being set st
( D1 = \$1 & D2 = \$2 & D2 c= D1 );
set Xm1 = { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } ;
set Xm = { S where S is Simplex of m, BCS (k,()) : verum } ;
consider R1 being Relation such that
A32: for x, y being object holds
( [x,y] in R1 iff ( x in { S where S is Simplex of m, BCS (k,()) : verum } & y in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } & S3[x,y] ) ) from set DY = (dom R1) \ YA;
A33: (dom R1) \ YA c= XX
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R1) \ YA or x in XX )
reconsider xx = x as set by TARSKI:1;
assume A34: x in (dom R1) \ YA ; :: thesis: x in XX
then consider y being object such that
A35: [x,y] in R1 by XTUPLE_0:def 12;
reconsider yy = y as set by TARSKI:1;
x in { S where S is Simplex of m, BCS (k,()) : verum } by ;
then consider S being Simplex of m, BCS (k,()) such that
A36: x = S and
verum ;
not x in YA by ;
then A37: F .: S <> Aa by A36;
y in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by ;
then A38: ex W being Simplex of m - 1, BCS (k,()) st
( y = W & Aa = F .: W ) ;
S3[xx,yy] by A32, A35;
then yy c= xx ;
then Aa c= F .: S by ;
then Aa c< F .: S by A37;
then m < card (F .: S) by ;
then A39: m + 1 <= card (F .: S) by NAT_1:13;
card (F .: S) <= m + 1 by ;
then F .: S = A by ;
hence x in XX by ; :: thesis: verum
end;
set RDY = R1 | ((dom R1) \ YA);
A40: (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) = {}
proof
assume (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) <> {} ; :: thesis: contradiction
then consider xy being object such that
A41: xy in (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) by XBOOLE_0:def 1;
consider x, y being object such that
A42: xy = [x,y] by ;
A43: x in (dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA) by ;
then ( dom (R1 | ((dom R1) \ YA)) c= (dom R1) \ YA & x in dom (R1 | ((dom R1) \ YA)) ) by RELAT_1:58;
hence contradiction by A43, XBOOLE_0:def 5; :: thesis: verum
end;
A44: 2 *` (card YA) = (card 2) *` (card (card YA))
.= card (2 * (card YA)) by CARD_2:39 ;
cA - 1 = (m + 1) + (- 1) by ;
then A45: degree () = m by SIMPLEX0:26;
consider R being Relation such that
A46: for x, y being object holds
( [x,y] in R iff ( x in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } & y in { S where S is Simplex of m, BCS (k,()) : verum } & S2[x,y] ) ) from A47: card R = card R1
proof
deffunc H1( object ) -> object = [(\$1 `2),(\$1 `1)];
A48: for x being object st x in R holds
H1(x) in R1
proof
let z be object ; :: thesis: ( z in R implies H1(z) in R1 )
assume A49: z in R ; :: thesis: H1(z) in R1
then ex x, y being object st z = [x,y] by RELAT_1:def 1;
then A50: z = [(z `1),(z `2)] ;
then A51: z `2 in { S where S is Simplex of m, BCS (k,()) : verum } by ;
( S2[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } ) by ;
hence H1(z) in R1 by ; :: thesis: verum
end;
consider f being Function of R,R1 such that
A52: for x being object st x in R holds
f . x = H1(x) from
per cases ( R1 is empty or not R1 is empty ) ;
suppose not R1 is empty ; :: thesis: card R = card R1
then A54: dom f = R by FUNCT_2:def 1;
R1 c= rng f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in R1 or z in rng f )
assume A55: z in R1 ; :: thesis: z in rng f
then ex x, y being object st z = [x,y] by RELAT_1:def 1;
then A56: z = [(z `1),(z `2)] ;
then A57: z `2 in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by ;
( S3[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m, BCS (k,()) : verum } ) by ;
then A58: [(z `2),(z `1)] in R by ;
H1([(z `2),(z `1)]) = z by A56;
then z = f . [(z `2),(z `1)] by ;
hence z in rng f by ; :: thesis: verum
end;
then A59: rng f = R1 ;
now :: thesis: for x1, x2 being object st x1 in R & x2 in R & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in R & x2 in R & f . x1 = f . x2 implies x1 = x2 )
assume that
A60: x1 in R and
A61: x2 in R and
A62: f . x1 = f . x2 ; :: thesis: x1 = x2
( f . x1 = H1(x1) & f . x2 = H1(x2) ) by ;
then A63: ( x1 `2 = x2 `2 & x1 `1 = x2 `1 ) by ;
A64: ex x, y being object st x2 = [x,y] by ;
ex x, y being object st x1 = [x,y] by ;
hence x1 = [(x2 `1),(x2 `2)] by A63
.= x2 by A64 ;
:: thesis: verum
end;
then f is one-to-one by ;
then R,R1 are_equipotent by ;
hence card R = card R1 by CARD_1:5; :: thesis: verum
end;
end;
end;
A65: ( |.(BCS (k,())).| = |.().| & |.().| = conv Aa ) by ;
set DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
A66: (dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= the topology of (BCS (k,()))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in the topology of (BCS (k,())) )
assume x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in the topology of (BCS (k,()))
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
then x in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by A46;
then ex S being Simplex of m - 1, BCS (k,()) st
( S = x & Aa = F .: S ) ;
hence x in the topology of (BCS (k,())) by PRE_TOPC:def 2; :: thesis: verum
end;
set RDX = R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } );
reconsider DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } as Subset-Family of (BCS (k,())) by ;
reconsider DX = DX as simplex-like Subset-Family of (BCS (k,())) by ;
A67: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) = {}
proof
assume (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) <> {} ; :: thesis: contradiction
then consider xy being object such that
A68: xy in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) by XBOOLE_0:def 1;
consider x, y being object such that
A69: xy = [x,y] by ;
A70: x in (dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX by ;
then ( dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) c= DX & x in dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) ) by RELAT_1:58;
hence contradiction by A70, XBOOLE_0:def 5; :: thesis: verum
end;
A71: m1 + 1 = (m - 1) + 1 by XXREAL_3:def 2
.= m ;
set FA = F | (Vertices (BCS (k,())));
A72: dom (F | (Vertices (BCS (k,())))) = Vertices (BCS (k,())) by ;
A73: not Vertices (BCS (k,())) is empty by A5, A6, A8, A30;
A74: for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= Aa & v in conv B holds
(F | (Vertices (BCS (k,())))) . v in B
proof
let v be Vertex of (BCS (k,())); :: thesis: for B being Subset of V st B c= Aa & v in conv B holds
(F | (Vertices (BCS (k,())))) . v in B

let B be Subset of V; :: thesis: ( B c= Aa & v in conv B implies (F | (Vertices (BCS (k,())))) . v in B )
assume A75: ( B c= Aa & v in conv B ) ; :: thesis: (F | (Vertices (BCS (k,())))) . v in B
v in Vertices (BCS (k,())) by A73;
then F . v in B by ;
hence (F | (Vertices (BCS (k,())))) . v in B by ; :: thesis: verum
end;
rng (F | (Vertices (BCS (k,())))) c= Aa
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (F | (Vertices (BCS (k,())))) or y in Aa )
assume y in rng (F | (Vertices (BCS (k,())))) ; :: thesis: y in Aa
then consider x being object such that
A76: x in dom (F | (Vertices (BCS (k,())))) and
A77: (F | (Vertices (BCS (k,())))) . x = y by FUNCT_1:def 3;
reconsider v = x as Element of (BCS (k,())) by ;
v is vertex-like by ;
then consider S being Subset of (BCS (k,())) such that
A78: S is simplex-like and
A79: v in S ;
A80: conv (@ S) c= |.(BCS (k,())).| by ;
S c= conv (@ S) by RLAFFIN1:2;
then A81: v in conv (@ S) by A79;
x in Vertices (BCS (k,())) by ;
hence y in Aa by A65, A74, A77, A80, A81; :: thesis: verum
end;
then reconsider FA = F | (Vertices (BCS (k,()))) as Function of (Vertices (BCS (k,()))),Aa by ;
set XXa = { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } ;
consider n being Nat such that
A82: card { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } = (2 * n) + 1 by A2, A5, A74;
A83: ( m - 1 <= m - 0 & - 1 <= m + (- 1) ) by ;
A84: for x being object st x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } holds
card (Im (R,x)) = 1
proof
let x be object ; :: thesis: ( x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } implies card (Im (R,x)) = 1 )
assume x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: card (Im (R,x)) = 1
then consider S being Simplex of m - 1, BCS (k,()) such that
A85: x = S and
A86: F .: S = Aa and
A87: conv (@ S) misses Int A ;
set XX = { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } ;
A88: R .: {S} c= { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 }
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in R .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } )
reconsider ww = w as set by TARSKI:1;
assume w in R .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 }
then consider s being object such that
A89: [s,w] in R and
A90: s in {S} by RELAT_1:def 13;
reconsider ss = s as set by TARSKI:1;
w in { S where S is Simplex of m, BCS (k,()) : verum } by ;
then A91: ex W being Simplex of m, BCS (k,()) st w = W ;
S2[ss,ww] by A46, A89;
then ( s = S & ss c= ww ) by ;
hence w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } by A91; :: thesis: verum
end;
{ S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } c= R .: {S}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } or w in R .: {S} )
assume w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } ; :: thesis: w in R .: {S}
then consider W being Simplex of m, BCS (k,()) such that
A92: w = W and
A93: S c= W ;
( W in { S where S is Simplex of m, BCS (k,()) : verum } & S in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } ) by A86;
then ( S in {S} & [S,W] in R ) by ;
hence w in R .: {S} by ; :: thesis: verum
end;
then A94: R .: {S} = { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } by A88;
card { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } = 1 by ;
hence card (Im (R,x)) = 1 by ; :: thesis: verum
end;
A95: degree () = degree (BCS (k,())) by ;
A96: M + 1 = m + 1 by XXREAL_3:def 2;
A97: for x being object st x in YA holds
card (Im (R1,x)) = 2
proof
let x be object ; :: thesis: ( x in YA implies card (Im (R1,x)) = 2 )
assume x in YA ; :: thesis: card (Im (R1,x)) = 2
then consider S being Simplex of m, BCS (k,()) such that
A98: x = S and
A99: Aa = F .: S ;
set FS = F | S;
A100: rng (F | S) = Aa by ;
A101: not Aa is empty by ;
A102: S in {x} by ;
A103: dom (F | S) = S by ;
A104: card S = m + 1 by ;
reconsider FS = F | S as Function of S,Aa by ;
FS is onto by ;
then consider b being set such that
A105: b in Aa and
A106: card (FS " {b}) = 2 and
A107: for x being set st x in Aa & x <> b holds
card (FS " {x}) = 1 by ;
consider a1, a2 being object such that
A108: a1 <> a2 and
A109: FS " {b} = {a1,a2} by ;
reconsider S1 = S \ {a1}, S2 = S \ {a2} as Simplex of (BCS (k,())) ;
A110: a1 in {a1,a2} by TARSKI:def 2;
then A111: a1 in S2 by ;
A112: card S1 = m by ;
A113: a2 in {a1,a2} by TARSKI:def 2;
then A114: card S2 = m by ;
then reconsider S1 = S1, S2 = S2 as Simplex of m - 1, BCS (k,()) by ;
A115: {a1} c= S by ;
A116: FS . a2 = F . a2 by ;
A117: {a2} c= S by ;
A118: R1 .: {x} c= {S1,S2}
proof
let Y be object ; :: according to TARSKI:def 3 :: thesis: ( not Y in R1 .: {x} or Y in {S1,S2} )
assume Y in R1 .: {x} ; :: thesis: Y in {S1,S2}
then consider X being object such that
A119: [X,Y] in R1 and
A120: X in {x} by RELAT_1:def 13;
Y in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by ;
then consider W being Simplex of m - 1, BCS (k,()) such that
A121: Y = W and
A122: Aa = F .: W ;
X = x by ;
then S3[S,W] by A32, A98, A119, A121;
then W c= S ;
then A123: Aa = FS .: W by ;
then consider w being object such that
A124: w in dom FS and
A125: w in W and
A126: FS . w = b by ;
A127: {w} c= W by ;
A128: S \ {a1,a2} c= W
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in S \ {a1,a2} or s in W )
assume A129: s in S \ {a1,a2} ; :: thesis: s in W
then A130: s in dom FS by ;
then A131: FS . s in Aa by ;
then consider w being object such that
A132: w in dom FS and
A133: w in W and
A134: FS . w = FS . s by ;
not s in FS " {b} by ;
then not FS . s in {b} by ;
then FS . s <> b by TARSKI:def 1;
then card (FS " {(FS . s)}) = 1 by ;
then consider z being object such that
A135: FS " {(FS . s)} = {z} by CARD_2:42;
A136: FS . s in {(FS . s)} by TARSKI:def 1;
then A137: s in FS " {(FS . s)} by ;
w in FS " {(FS . s)} by ;
then w = z by ;
hence s in W by ; :: thesis: verum
end;
b in {b} by TARSKI:def 1;
then A138: w in FS " {b} by ;
A139: card W = m by ;
A140: S /\ {a1} = {a1} by ;
A141: S /\ {a2} = {a2} by ;
per cases ( w = a1 or w = a2 ) by ;
suppose w = a1 ; :: thesis: Y in {S1,S2}
then (S \ {a1,a2}) \/ {w} = S \ ({a1,a2} \ {a1}) by
.= S2 by ;
then S2 = W by ;
hence Y in {S1,S2} by ; :: thesis: verum
end;
suppose w = a2 ; :: thesis: Y in {S1,S2}
then (S \ {a1,a2}) \/ {w} = S \ ({a1,a2} \ {a2}) by
.= S1 by ;
then S1 = W by ;
hence Y in {S1,S2} by ; :: thesis: verum
end;
end;
end;
A142: S c= dom F by ;
A143: FS . a1 = F . a1 by ;
A144: FS . a1 in {b} by ;
then A145: FS . a1 = b by TARSKI:def 1;
A146: FS . a2 in {b} by ;
then A147: FS . a2 = b by TARSKI:def 1;
A148: ( a2 in S & a2 in S1 ) by ;
A149: Aa c= F .: S1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Aa or z in F .: S1 )
assume A150: z in Aa ; :: thesis: z in F .: S1
per cases ( z = b or z <> b ) ;
suppose A151: z = b ; :: thesis: z in F .: S1
FS . a2 in F .: S1 by ;
hence z in F .: S1 by ; :: thesis: verum
end;
suppose A152: z <> b ; :: thesis: z in F .: S1
consider c being object such that
A153: c in dom F and
A154: c in S and
A155: z = F . c by ;
c in S1 by ;
hence z in F .: S1 by ; :: thesis: verum
end;
end;
end;
A156: S in { S where S is Simplex of m, BCS (k,()) : verum } ;
A157: ( a1 in S & a1 in S2 ) by ;
A158: Aa c= F .: S2
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Aa or z in F .: S2 )
assume A159: z in Aa ; :: thesis: z in F .: S2
per cases ( z = b or z <> b ) ;
suppose A160: z = b ; :: thesis: z in F .: S2
FS . a1 in F .: S2 by ;
hence z in F .: S2 by ; :: thesis: verum
end;
suppose A161: z <> b ; :: thesis: z in F .: S2
consider c being object such that
A162: c in dom F and
A163: c in S and
A164: z = F . c by ;
c in S2 by ;
hence z in F .: S2 by ; :: thesis: verum
end;
end;
end;
F .: S1 c= Aa by ;
then Aa = F .: S1 by A149;
then ( S \ {a1} c= S & S1 in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } ) by XBOOLE_1:36;
then [S,S1] in R1 by ;
then A165: S1 in R1 .: {x} by ;
F .: S2 c= Aa by ;
then Aa = F .: S2 by A158;
then ( S \ {a2} c= S & S2 in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } ) by XBOOLE_1:36;
then [S,S2] in R1 by ;
then S2 in R1 .: {x} by ;
then {S1,S2} c= R1 .: {x} by ;
then A166: R1 .: {x} = {S1,S2} by A118;
S1 <> S2 by ;
then card (R1 .: {x}) = 2 by ;
hence card (Im (R1,x)) = 2 by RELAT_1:def 16; :: thesis: verum
end;
A167: M - 1 = m + (- 1) by XXREAL_3:def 2;
XX c= (dom R1) \ YA
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX or x in (dom R1) \ YA )
assume x in XX ; :: thesis: x in (dom R1) \ YA
then consider S being Simplex of m, BCS (k,()) such that
A168: x = S and
A169: F .: S = A by A3;
set FS = F | S;
A170: rng (F | S) = A by ;
A171: card A = card S by ;
A172: dom (F | S) = S by ;
then reconsider FS = F | S as Function of S,A by ;
consider s being object such that
A173: ( s in dom FS & FS . s = a ) by ;
set Ss = S \ {s};
FS is onto by ;
then A174: FS is one-to-one by ;
then A175: FS .: (S \ {s}) = (FS .: S) \ (FS .: {s}) by FUNCT_1:64
.= A \ (FS .: {s}) by
.= A \ (Im (FS,s)) by RELAT_1:def 16
.= Aa by ;
S \ {s},FS .: (S \ {s}) are_equipotent by ;
then A176: card (S \ {s}) = m by ;
reconsider Ss = S \ {s} as Simplex of (BCS (k,())) ;
reconsider Ss = Ss as Simplex of m - 1, BCS (k,()) by ;
FS .: Ss = F .: Ss by ;
then A177: Ss in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by A175;
( Ss c= S & S in { S where S is Simplex of m, BCS (k,()) : verum } ) by XBOOLE_1:36;
then [S,Ss] in R1 by ;
then A178: S in dom R1 by XTUPLE_0:def 12;
for W being Simplex of m, BCS (k,()) st S = W holds
Aa <> F .: W by ;
then not S in YA ;
hence x in (dom R1) \ YA by ; :: thesis: verum
end;
then A179: (dom R1) \ YA = XX by A33;
for x being object st x in (dom R1) \ YA holds
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
proof
let x be object ; :: thesis: ( x in (dom R1) \ YA implies card (Im ((R1 | ((dom R1) \ YA)),x)) = 1 )
assume A180: x in (dom R1) \ YA ; :: thesis: card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
then consider y being object such that
A181: [x,y] in R1 by XTUPLE_0:def 12;
A182: ex W being Simplex of m, BCS (k,()) st
( x = W & F .: W = A ) by ;
x in { S where S is Simplex of m, BCS (k,()) : verum } by ;
then consider S being Simplex of m, BCS (k,()) such that
A183: x = S and
verum ;
y in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by ;
then consider W being Simplex of m - 1, BCS (k,()) such that
A184: y = W and
A185: Aa = F .: W ;
A186: card S = m + 1 by ;
A187: (R1 | ((dom R1) \ YA)) .: {x} c= {y}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (R1 | ((dom R1) \ YA)) .: {x} or u in {y} )
set FS = F | S;
assume u in (R1 | ((dom R1) \ YA)) .: {x} ; :: thesis: u in {y}
then consider s being object such that
A188: [s,u] in R1 | ((dom R1) \ YA) and
A189: s in {x} by RELAT_1:def 13;
A190: [s,u] in R1 by ;
then u in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by A32;
then consider U being Simplex of m - 1, BCS (k,()) such that
A191: u = U and
A192: Aa = F .: U ;
A193: dom (F | S) = S by ;
A194: rng (F | S) = A by ;
then reconsider FS = F | S as Function of S,A by ;
S3[S,W] by A32, A181, A183, A184;
then A195: W c= S ;
then A196: FS .: W = F .: W by RELAT_1:129;
s = S by ;
then S3[S,U] by A32, A190, A191;
then A197: U c= S ;
then A198: FS .: U = F .: U by RELAT_1:129;
FS is onto by ;
then A199: FS is one-to-one by ;
then A200: U c= W by ;
W c= U by ;
then u = y by ;
hence u in {y} by TARSKI:def 1; :: thesis: verum
end;
( x in {x} & [x,y] in R1 | ((dom R1) \ YA) ) by ;
then y in (R1 | ((dom R1) \ YA)) .: {x} by RELAT_1:def 13;
then (R1 | ((dom R1) \ YA)) .: {x} = {y} by ;
then Im ((R1 | ((dom R1) \ YA)),x) = {y} by RELAT_1:def 16;
hence card (Im ((R1 | ((dom R1) \ YA)),x)) = 1 by CARD_1:30; :: thesis: verum
end;
then card (R1 | ((dom R1) \ YA)) = () +` (1 *` (card ((dom R1) \ YA))) by
.= 1 *` (card ((dom R1) \ YA)) by CARD_2:18
.= card ((dom R1) \ YA) by CARD_2:21 ;
then A201: card R1 = (card (card XX)) +` (card (2 * (card YA))) by
.= card ((card XX) + (2 * (card YA))) by CARD_2:38
.= (card XX) + (2 * (card YA)) ;
A202: ( |.(BCS (k,())).| = |.().| & |.().| = conv A ) by ;
A203: { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } )
assume x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa }
then consider S being Simplex of m - 1, BCS (k,()) such that
A204: x = S and
A205: F .: S = Aa and
A206: conv (@ S) misses Int A ;
conv (@ S) c= conv A by ;
then consider B being Subset of V such that
A207: B c< A and
A208: conv (@ S) c= conv B by ;
A209: B c= A by A207;
then reconsider B = B as finite Subset of V ;
card B < m + 1 by ;
then A210: card B <= m by NAT_1:13;
A211: Aa c= B
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Aa or y in B )
assume y in Aa ; :: thesis: y in B
then consider v being object such that
A212: v in dom F and
A213: v in S and
A214: F . v = y by ;
S c= conv (@ S) by RLAFFIN1:2;
then v in conv (@ S) by A213;
hence y in B by ; :: thesis: verum
end;
then card Aa <= card B by NAT_1:43;
then A215: Aa = B by ;
A216: the topology of (BCS (k,())) c= the topology of (BCS (k,())) by ;
A217: card S = m by ;
then not S is empty by A30;
then A218: (center_of_mass V) . S in Int (@ S) by RLAFFIN2:20;
Int (@ S) c= conv (@ S) by RLAFFIN2:5;
then (center_of_mass V) . S in conv (@ S) by A218;
then consider w being Subset of (BCS (k,())) such that
A219: w is simplex-like and
A220: (center_of_mass V) . S in conv (@ w) by ;
w in the topology of (BCS (k,())) by A219;
then w in the topology of (BCS (k,())) by A216;
then reconsider W = w as Simplex of (BCS (k,())) by PRE_TOPC:def 2;
Int (@ S) meets conv (@ W) by ;
then A221: S c= w by Th26;
then reconsider s = S as Subset of (BCS (k,())) by XBOOLE_1:1;
reconsider s = s as Simplex of (BCS (k,())) by ;
A222: FA .: s = Aa by ;
s is Simplex of m - 1, BCS (k,()) by ;
hence x in { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } by ; :: thesis: verum
end;
A223: degree () = m - 1 by ;
{ S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } c= { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) }
proof
A <> Aa by A3, A5;
then A224: Aa c< A by A12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } or x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )
assume x in { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) }
then consider S being Simplex of m - 1, BCS (k,()) such that
A225: x = S and
A226: FA .: S = Aa ;
m - 1 <= degree (BCS (k,())) by ;
then reconsider S1 = x as Simplex of m - 1, BCS (k,()) by ;
A227: FA .: S = F .: S by ;
conv (@ S) c= conv Aa by ;
then conv (@ S1) misses Int A by ;
hence x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } by ; :: thesis: verum
end;
then A228: { S where S is Simplex of m - 1, BCS (k,()) : FA .: S = Aa } = { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A203;
for x being object st x in DX holds
card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
proof
let x be object ; :: thesis: ( x in DX implies card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 )
assume A229: x in DX ; :: thesis: card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
then A230: x in { S where S is Simplex of m - 1, BCS (k,()) : Aa = F .: S } by A46;
then consider S being Simplex of m - 1, BCS (k,()) such that
A231: x = S and
A232: Aa = F .: S ;
set XX = { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } ;
not x in { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } by ;
then conv (@ S) meets Int A by ;
then A233: card { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } = 2 by ;
A234: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} c= { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 }
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } )
reconsider ww = w as set by TARSKI:1;
assume w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 }
then consider s being object such that
A235: [s,w] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) and
A236: s in {S} by RELAT_1:def 13;
A237: [s,w] in R by ;
then w in { S where S is Simplex of m, BCS (k,()) : verum } by A46;
then A238: ex W being Simplex of m, BCS (k,()) st w = W ;
s = S by ;
then S2[S,ww] by A46, A237;
then S c= ww ;
hence w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } by A238; :: thesis: verum
end;
{ S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } c= (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } or w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} )
assume w in { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } ; :: thesis: w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
then consider W being Simplex of m, BCS (k,()) such that
A239: w = W and
A240: S c= W ;
W in { S where S is Simplex of m, BCS (k,()) : verum } ;
then [S,W] in R by ;
then A241: [S,W] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) by ;
S in {S} by TARSKI:def 1;
hence w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by ; :: thesis: verum
end;
then { S1 where S1 is Simplex of m, BCS (k,()) : S c= S1 } = (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by A234;
hence card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 by ; :: thesis: verum
end;
then card (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) = (card ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX))) +` (2 *` (card DX)) by Th1
.= 0 +` (2 *` (card DX)) by A67
.= 2 *` (card DX) by CARD_2:18 ;
then A242: card R = (2 *` (card DX)) +` (1 *` (card { S where S is Simplex of m - 1, BCS (k,()) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) by
.= (2 *` (card DX)) +` ((2 * n) + 1) by
.= ((card 2) *` (card (card DX))) +` ((2 * n) + 1)
.= (card (2 * (card DX))) +` ((2 * n) + 1) by CARD_2:39
.= (card (2 * (card DX))) +` (card ((2 * n) + 1))
.= card ((2 * (card DX)) + ((2 * n) + 1)) by CARD_2:38
.= (2 * (card DX)) + ((2 * n) + 1) ;
then card XX = (2 * (((card DX) + n) - (card YA))) + 1 by ;
then 2 * (((card DX) + n) - (card YA)) >= - 1 by INT_1:7;
then ((card DX) + n) - (card YA) >= (- 1) / 2 by XREAL_1:79;
then ((card DX) + n) - (card YA) > - 1 by XXREAL_0:2;
then ((card DX) + n) - (card YA) >= 0 by INT_1:8;
then reconsider cnc = ((card DX) + n) - (card YA) as Element of NAT by INT_1:3;
take cnc ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * cnc) + 1
thus card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * cnc) + 1 by ; :: thesis: verum
end;
end;
end;
A243: S1[ 0 ]
proof
let A be finite affinely-independent Subset of V; :: thesis: ( card A = 0 implies for F being Function of (Vertices (BCS (k,()))),A st ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1 )

assume A244: card A = 0 ; :: thesis: for F being Function of (Vertices (BCS (k,()))),A st ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1

A245: A = {} by A244;
set C = Complex_of {A};
A246: ( |.().| c= [#] V & [#] () = [#] V ) ;
let F be Function of (Vertices (BCS (k,()))),A; :: thesis: ( ( for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1 )

assume for v being Vertex of (BCS (k,()))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * n) + 1
set X = { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } ;
take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * 0) + 1
A247: ( k = 0 or k > 0 ) ;
A248: Z - 1 = - 1 by XXREAL_3:4;
then degree () = - 1 by ;
then A249: Complex_of {A} = BCS (k,()) by ;
A250: the topology of () = bool A by SIMPLEX0:4;
A251: { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } c= {A}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } or x in {A} )
assume A252: x in { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } ; :: thesis: x in {A}
consider S being Simplex of (card A) - 1, BCS (k,()) such that
A253: S = x and
F .: S = A by A252;
S in the topology of () by ;
then S is empty by ;
hence x in {A} by ; :: thesis: verum
end;
A in bool A by ZFMISC_1:def 1;
then reconsider A1 = A as Simplex of () by ;
A254: F .: A1 = A by A245;
A1 is Simplex of - 1, Complex_of {A} by ;
then A in { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } by ;
then { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = {A} by ;
hence card { S where S is Simplex of (card A) - 1, BCS (k,()) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum
end;
for k being Nat holds S1[k] from hence 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 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 ; :: thesis: verum