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 S_{1}[ Nat] means for A being finite affinely-independent Subset of V st card A = $1 holds

for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1;

A1: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A243, A1);

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

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 S

for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1;

A1: for m being Nat st S

S

proof

A243:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A2: S_{1}[m]
; :: thesis: S_{1}[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,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A3: card A = m + 1 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : 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 A3, A4, STIRL2_1:55;

reconsider Aa = A \ {a} as finite affinely-independent Subset of V by RLAFFIN1:43, XBOOLE_1:36;

set CAa = Complex_of {Aa};

the topology of (Complex_of {Aa}) = bool Aa by SIMPLEX0:4;

then A6: Vertices (Complex_of {Aa}) = union (bool Aa) by SIMPLEX0:16

.= Aa by ZFMISC_1:81 ;

A7: ( [#] (Complex_of {Aa}) = [#] V & |.(Complex_of {Aa}).| c= [#] V ) ;

then A8: Vertices (Complex_of {Aa}) c= Vertices (BCS (k,(Complex_of {Aa}))) by Th24;

set CA = Complex_of {A};

let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A9: for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

set XX = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;

A10: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= the topology of (BCS (k,(Complex_of {A})))

reconsider XX = XX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A10, SIMPLEX0:14;

A11: ( [#] (Complex_of {A}) = [#] V & |.(Complex_of {A}).| 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 )

then Complex_of {Aa} is SubSimplicialComplex of Complex_of {A} by SIMPLEX0:30;

then A14: BCS (k,(Complex_of {Aa})) is SubSimplicialComplex of BCS (k,(Complex_of {A})) by A11, A7, Th23;

then A15: Vertices (BCS (k,(Complex_of {Aa}))) c= Vertices (BCS (k,(Complex_of {A}))) by SIMPLEX0:31;

A16: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;

then A17: Vertices (Complex_of {A}) = union (bool A) by SIMPLEX0:16

.= A by ZFMISC_1:81 ;

A18: dom F = Vertices (BCS (k,(Complex_of {A}))) by A4, FUNCT_2:def 1;

end;assume A2: S

let A be finite affinely-independent Subset of V; :: thesis: ( card A = m + 1 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A3: card A = m + 1 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : 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 A3, A4, STIRL2_1:55;

reconsider Aa = A \ {a} as finite affinely-independent Subset of V by RLAFFIN1:43, XBOOLE_1:36;

set CAa = Complex_of {Aa};

the topology of (Complex_of {Aa}) = bool Aa by SIMPLEX0:4;

then A6: Vertices (Complex_of {Aa}) = union (bool Aa) by SIMPLEX0:16

.= Aa by ZFMISC_1:81 ;

A7: ( [#] (Complex_of {Aa}) = [#] V & |.(Complex_of {Aa}).| c= [#] V ) ;

then A8: Vertices (Complex_of {Aa}) c= Vertices (BCS (k,(Complex_of {Aa}))) by Th24;

set CA = Complex_of {A};

let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A9: for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

set XX = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;

A10: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= the topology of (BCS (k,(Complex_of {A})))

proof

then reconsider XX = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } as Subset-Family of (BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } or x in the topology of (BCS (k,(Complex_of {A}))) )

assume x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

then ex S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) st

( S = x & A = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

end;assume x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

then ex S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) st

( S = x & A = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

reconsider XX = XX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A10, SIMPLEX0:14;

A11: ( [#] (Complex_of {A}) = [#] V & |.(Complex_of {A}).| 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

then
{Aa} is_finer_than {A}
;
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 A12, A13, TARSKI:def 1; :: thesis: verum

end;( 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 A12, A13, TARSKI:def 1; :: thesis: verum

then Complex_of {Aa} is SubSimplicialComplex of Complex_of {A} by SIMPLEX0:30;

then A14: BCS (k,(Complex_of {Aa})) is SubSimplicialComplex of BCS (k,(Complex_of {A})) by A11, A7, Th23;

then A15: Vertices (BCS (k,(Complex_of {Aa}))) c= Vertices (BCS (k,(Complex_of {A}))) by SIMPLEX0:31;

A16: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;

then A17: Vertices (Complex_of {A}) = union (bool A) by SIMPLEX0:16

.= A by ZFMISC_1:81 ;

A18: dom F = Vertices (BCS (k,(Complex_of {A}))) by A4, FUNCT_2:def 1;

per cases
( m = 0 or m > 0 )
;

end;

suppose A19:
m = 0
; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

A20:
O - 1 = 0
by XXREAL_3:7;

then A21: degree (Complex_of {A}) = 0 by A3, A19, SIMPLEX0:26;

( k = 0 or k > 0 ) ;

then A22: BCS (k,(Complex_of {A})) = Complex_of {A} by A11, A21, Th16, Th22;

then A23: dom F = Vertices (Complex_of {A}) by A4, FUNCT_2:def 1;

take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1

A in bool A by ZFMISC_1:def 1;

then reconsider A1 = A as Simplex of (Complex_of {A}) by A16, PRE_TOPC:def 2;

A24: A1 is Simplex of 0 , Complex_of {A} by A3, A19, A20, SIMPLEX0:48;

ex x being object st A = {x} by A3, A19, CARD_2:42;

then A25: A = {a} by A4, TARSKI:def 1;

then conv A = A by RLAFFIN1:1;

then F . a in A by A4, A9, A17, A22;

then A26: F . a = a by A25, TARSKI:def 1;

A27: XX c= {A}

.= A by A4, A17, A23, A25, A26, FUNCT_1:59 ;

then A in XX by A3, A19, A24, A22;

then XX = {A} by A27, ZFMISC_1:33;

hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum

end;then A21: degree (Complex_of {A}) = 0 by A3, A19, SIMPLEX0:26;

( k = 0 or k > 0 ) ;

then A22: BCS (k,(Complex_of {A})) = Complex_of {A} by A11, A21, Th16, Th22;

then A23: dom F = Vertices (Complex_of {A}) by A4, FUNCT_2:def 1;

take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1

A in bool A by ZFMISC_1:def 1;

then reconsider A1 = A as Simplex of (Complex_of {A}) by A16, PRE_TOPC:def 2;

A24: A1 is Simplex of 0 , Complex_of {A} by A3, A19, A20, SIMPLEX0:48;

ex x being object st A = {x} by A3, A19, CARD_2:42;

then A25: A = {a} by A4, TARSKI:def 1;

then conv A = A by RLAFFIN1:1;

then F . a in A by A4, A9, A17, A22;

then A26: F . a = a by A25, TARSKI:def 1;

A27: XX c= {A}

proof

F .: A =
Im (F,a)
by A25, RELAT_1:def 16
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 (Complex_of {A}) by PRE_TOPC:def 2;

card S = Z + 1 by A21, SIMPLEX0:def 18

.= 1 by XXREAL_3:4 ;

then S = A by A3, A16, A19, A29, CARD_2:102;

hence x in {A} by A28, TARSKI:def 1; :: thesis: verum

end;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 (Complex_of {A}) by PRE_TOPC:def 2;

card S = Z + 1 by A21, SIMPLEX0:def 18

.= 1 by XXREAL_3:4 ;

then S = A by A3, A16, A19, A29, CARD_2:102;

hence x in {A} by A28, TARSKI:def 1; :: thesis: verum

.= A by A4, A17, A23, A25, A26, FUNCT_1:59 ;

then A in XX by A3, A19, A24, A22;

then XX = {A} by A27, ZFMISC_1:33;

hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum

suppose A30:
m > 0
; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

defpred S_{2}[ 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,(Complex_of {A})) : ( 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,(Complex_of {A})) : Aa = F .: S } ;

A31: { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } c= the topology of (BCS (k,(Complex_of {A})))

reconsider YA = YA as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A31, SIMPLEX0:14;

defpred S_{3}[ 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,(Complex_of {A})) : Aa = F .: S } ;

set Xm = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : 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,(Complex_of {A})) : verum } & y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } & S_{3}[x,y] ) )
from RELAT_1:sch 1();

set DY = (dom R1) \ YA;

A33: (dom R1) \ YA c= XX

A40: (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) = {}

.= card (2 * (card YA)) by CARD_2:39 ;

cA - 1 = (m + 1) + (- 1) by A3, XXREAL_3:def 2;

then A45: degree (Complex_of {A}) = 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,(Complex_of {A})) : Aa = F .: S } & y in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S_{2}[x,y] ) )
from RELAT_1:sch 1();

A47: card R = card R1

set DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;

A66: (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= the topology of (BCS (k,(Complex_of {A})))

reconsider DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } as Subset-Family of (BCS (k,(Complex_of {A}))) by A66, XBOOLE_1:1;

reconsider DX = DX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A66, SIMPLEX0:14;

A67: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) = {}

.= m ;

set FA = F | (Vertices (BCS (k,(Complex_of {Aa}))));

A72: dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) = Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, RELAT_1:62, SIMPLEX0:31;

A73: not Vertices (BCS (k,(Complex_of {Aa}))) is empty by A5, A6, A8, A30;

A74: for v being Vertex of (BCS (k,(Complex_of {Aa})))

for B being Subset of V st B c= Aa & v in conv B holds

(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

set XXa = { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ;

consider n being Nat such that

A82: card { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = (2 * n) + 1 by A2, A5, A74;

A83: ( m - 1 <= m - 0 & - 1 <= m + (- 1) ) by XREAL_1:10, XREAL_1:31;

A84: for x being object st x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } holds

card (Im (R,x)) = 1

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

XX c= (dom R1) \ YA

for x being object st x in (dom R1) \ YA holds

card (Im ((R1 | ((dom R1) \ YA)),x)) = 1

.= 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 A44, A97, A179, Th1

.= card ((card XX) + (2 * (card YA))) by CARD_2:38

.= (card XX) + (2 * (card YA)) ;

A202: ( |.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| & |.(Complex_of {A}).| = conv A ) by Th8, Th10;

A203: { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }

{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }

for x being object st x in DX holds

card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2

.= 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) by A84, Th1

.= (2 *` (card DX)) +` ((2 * n) + 1) by A82, A228, CARD_2:21

.= ((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 A47, A201;

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,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1

thus card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1 by A47, A201, A242; :: thesis: verum

end;( D1 = $1 & D2 = $2 & D1 c= D2 );

set XXA = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : Aa = F .: S } ;

A31: { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } c= the topology of (BCS (k,(Complex_of {A})))

proof

then reconsider YA = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } as Subset-Family of (BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } or x in the topology of (BCS (k,(Complex_of {A}))) )

assume x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

then ex S being Simplex of m, BCS (k,(Complex_of {A})) st

( S = x & Aa = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

end;assume x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

then ex S being Simplex of m, BCS (k,(Complex_of {A})) st

( S = x & Aa = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

reconsider YA = YA as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A31, SIMPLEX0:14;

defpred S

( D1 = $1 & D2 = $2 & D2 c= D1 );

set Xm1 = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ;

set Xm = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : 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,(Complex_of {A})) : verum } & y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } & S

set DY = (dom R1) \ YA;

A33: (dom R1) \ YA c= XX

proof

set RDY = R1 | ((dom R1) \ YA);
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,(Complex_of {A})) : verum } by A32, A35;

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A36: x = S and

verum ;

not x in YA by A34, XBOOLE_0:def 5;

then A37: F .: S <> Aa by A36;

y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A35;

then A38: ex W being Simplex of m - 1, BCS (k,(Complex_of {A})) st

( y = W & Aa = F .: W ) ;

S_{3}[xx,yy]
by A32, A35;

then yy c= xx ;

then Aa c= F .: S by A36, A38, RELAT_1:123;

then Aa c< F .: S by A37;

then m < card (F .: S) by A5, CARD_2:48;

then A39: m + 1 <= card (F .: S) by NAT_1:13;

card (F .: S) <= m + 1 by A3, NAT_1:43;

then F .: S = A by A3, A39, CARD_2:102, XXREAL_0:1;

hence x in XX by A3, A36; :: thesis: verum

end;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,(Complex_of {A})) : verum } by A32, A35;

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A36: x = S and

verum ;

not x in YA by A34, XBOOLE_0:def 5;

then A37: F .: S <> Aa by A36;

y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A35;

then A38: ex W being Simplex of m - 1, BCS (k,(Complex_of {A})) st

( y = W & Aa = F .: W ) ;

S

then yy c= xx ;

then Aa c= F .: S by A36, A38, RELAT_1:123;

then Aa c< F .: S by A37;

then m < card (F .: S) by A5, CARD_2:48;

then A39: m + 1 <= card (F .: S) by NAT_1:13;

card (F .: S) <= m + 1 by A3, NAT_1:43;

then F .: S = A by A3, A39, CARD_2:102, XXREAL_0:1;

hence x in XX by A3, A36; :: thesis: verum

A40: (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) = {}

proof

A44: 2 *` (card YA) =
(card 2) *` (card (card YA))
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 A41, RELAT_1:def 1;

A43: x in (dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA) by A41, A42, RELAT_1:def 11;

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;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 A41, RELAT_1:def 1;

A43: x in (dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA) by A41, A42, RELAT_1:def 11;

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

.= card (2 * (card YA)) by CARD_2:39 ;

cA - 1 = (m + 1) + (- 1) by A3, XXREAL_3:def 2;

then A45: degree (Complex_of {A}) = 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,(Complex_of {A})) : Aa = F .: S } & y in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S

A47: card R = card R1

proof

A65:
( |.(BCS (k,(Complex_of {Aa}))).| = |.(Complex_of {Aa}).| & |.(Complex_of {Aa}).| = conv Aa )
by Th8, Th10;
deffunc H_{1}( object ) -> object = [($1 `2),($1 `1)];

A48: for x being object st x in R holds

H_{1}(x) in R1

A52: for x being object st x in R holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A48);

end;A48: for x being object st x in R holds

H

proof

consider f being Function of R,R1 such that
let z be object ; :: thesis: ( z in R implies H_{1}(z) in R1 )

assume A49: z in R ; :: thesis: H_{1}(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,(Complex_of {A})) : verum } by A46, A49;

( S_{2}[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } )
by A46, A49, A50;

hence H_{1}(z) in R1
by A32, A51; :: thesis: verum

end;assume A49: z in R ; :: thesis: H

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,(Complex_of {A})) : verum } by A46, A49;

( S

hence H

A52: for x being object st x in R holds

f . x = H

per cases
( R1 is empty or not R1 is empty )
;

end;

suppose
not R1 is empty
; :: thesis: card R = card R1

then A54:
dom f = R
by FUNCT_2:def 1;

R1 c= rng f

then R,R1 are_equipotent by A54, A59, WELLORD2:def 4;

hence card R = card R1 by CARD_1:5; :: thesis: verum

end;R1 c= rng f

proof

then A59:
rng f = R1
;
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,(Complex_of {A})) : Aa = F .: S } by A32, A55;

( S_{3}[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } )
by A32, A55, A56;

then A58: [(z `2),(z `1)] in R by A46, A57;

H_{1}([(z `2),(z `1)]) = z
by A56;

then z = f . [(z `2),(z `1)] by A52, A58;

hence z in rng f by A54, A58, FUNCT_1:def 3; :: thesis: verum

end;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,(Complex_of {A})) : Aa = F .: S } by A32, A55;

( S

then A58: [(z `2),(z `1)] in R by A46, A57;

H

then z = f . [(z `2),(z `1)] by A52, A58;

hence z in rng f by A54, A58, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for x1, x2 being object st x1 in R & x2 in R & f . x1 = f . x2 holds

x1 = x2

then
f is one-to-one
by A54, FUNCT_1:def 4;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 = H_{1}(x1) & f . x2 = H_{1}(x2) )
by A52, A60, A61;

then A63: ( x1 `2 = x2 `2 & x1 `1 = x2 `1 ) by A62, XTUPLE_0:1;

A64: ex x, y being object st x2 = [x,y] by A61, RELAT_1:def 1;

ex x, y being object st x1 = [x,y] by A60, RELAT_1:def 1;

hence x1 = [(x2 `1),(x2 `2)] by A63

.= x2 by A64 ;

:: thesis: verum

end;assume that

A60: x1 in R and

A61: x2 in R and

A62: f . x1 = f . x2 ; :: thesis: x1 = x2

( f . x1 = H

then A63: ( x1 `2 = x2 `2 & x1 `1 = x2 `1 ) by A62, XTUPLE_0:1;

A64: ex x, y being object st x2 = [x,y] by A61, RELAT_1:def 1;

ex x, y being object st x1 = [x,y] by A60, RELAT_1:def 1;

hence x1 = [(x2 `1),(x2 `2)] by A63

.= x2 by A64 ;

:: thesis: verum

then R,R1 are_equipotent by A54, A59, WELLORD2:def 4;

hence card R = card R1 by CARD_1:5; :: thesis: verum

set DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;

A66: (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= the topology of (BCS (k,(Complex_of {A})))

proof

set RDX = R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } );
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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in the topology of (BCS (k,(Complex_of {A}))) )

assume x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : Aa = F .: S } by A46;

then ex S being Simplex of m - 1, BCS (k,(Complex_of {A})) st

( S = x & Aa = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

end;assume x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : Aa = F .: S } by A46;

then ex S being Simplex of m - 1, BCS (k,(Complex_of {A})) st

( S = x & Aa = F .: S ) ;

hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum

reconsider DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } as Subset-Family of (BCS (k,(Complex_of {A}))) by A66, XBOOLE_1:1;

reconsider DX = DX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A66, SIMPLEX0:14;

A67: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) = {}

proof

A71: m1 + 1 =
(m - 1) + 1
by XXREAL_3:def 2
assume
(R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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 A68, RELAT_1:def 1;

A70: x in (dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX by A68, A69, RELAT_1:def 11;

then ( dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) ) by RELAT_1:58;

hence contradiction by A70, XBOOLE_0:def 5; :: thesis: verum

end;then consider xy being object such that

A68: xy in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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 A68, RELAT_1:def 1;

A70: x in (dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX by A68, A69, RELAT_1:def 11;

then ( dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) ) by RELAT_1:58;

hence contradiction by A70, XBOOLE_0:def 5; :: thesis: verum

.= m ;

set FA = F | (Vertices (BCS (k,(Complex_of {Aa}))));

A72: dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) = Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, RELAT_1:62, SIMPLEX0:31;

A73: not Vertices (BCS (k,(Complex_of {Aa}))) is empty by A5, A6, A8, A30;

A74: for v being Vertex of (BCS (k,(Complex_of {Aa})))

for B being Subset of V st B c= Aa & v in conv B holds

(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

proof

rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) c= Aa
let v be Vertex of (BCS (k,(Complex_of {Aa}))); :: thesis: for B being Subset of V st B c= Aa & v in conv B holds

(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

let B be Subset of V; :: thesis: ( B c= Aa & v in conv B implies (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B )

assume A75: ( B c= Aa & v in conv B ) ; :: thesis: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

v in Vertices (BCS (k,(Complex_of {Aa}))) by A73;

then F . v in B by A9, A12, A15, A75, XBOOLE_1:1;

hence (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B by A72, A73, FUNCT_1:47; :: thesis: verum

end;(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

let B be Subset of V; :: thesis: ( B c= Aa & v in conv B implies (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B )

assume A75: ( B c= Aa & v in conv B ) ; :: thesis: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B

v in Vertices (BCS (k,(Complex_of {Aa}))) by A73;

then F . v in B by A9, A12, A15, A75, XBOOLE_1:1;

hence (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B by A72, A73, FUNCT_1:47; :: thesis: verum

proof

then reconsider FA = F | (Vertices (BCS (k,(Complex_of {Aa})))) as Function of (Vertices (BCS (k,(Complex_of {Aa})))),Aa by A72, FUNCT_2:2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) or y in Aa )

assume y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) ; :: thesis: y in Aa

then consider x being object such that

A76: x in dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) and

A77: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . x = y by FUNCT_1:def 3;

reconsider v = x as Element of (BCS (k,(Complex_of {Aa}))) by A72, A76;

v is vertex-like by A72, A76, SIMPLEX0:def 4;

then consider S being Subset of (BCS (k,(Complex_of {Aa}))) such that

A78: S is simplex-like and

A79: v in S ;

A80: conv (@ S) c= |.(BCS (k,(Complex_of {Aa}))).| by A78, Th5;

S c= conv (@ S) by RLAFFIN1:2;

then A81: v in conv (@ S) by A79;

x in Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, A76, RELAT_1:62, SIMPLEX0:31;

hence y in Aa by A65, A74, A77, A80, A81; :: thesis: verum

end;assume y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) ; :: thesis: y in Aa

then consider x being object such that

A76: x in dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) and

A77: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . x = y by FUNCT_1:def 3;

reconsider v = x as Element of (BCS (k,(Complex_of {Aa}))) by A72, A76;

v is vertex-like by A72, A76, SIMPLEX0:def 4;

then consider S being Subset of (BCS (k,(Complex_of {Aa}))) such that

A78: S is simplex-like and

A79: v in S ;

A80: conv (@ S) c= |.(BCS (k,(Complex_of {Aa}))).| by A78, Th5;

S c= conv (@ S) by RLAFFIN1:2;

then A81: v in conv (@ S) by A79;

x in Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, A76, RELAT_1:62, SIMPLEX0:31;

hence y in Aa by A65, A74, A77, A80, A81; :: thesis: verum

set XXa = { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ;

consider n being Nat such that

A82: card { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = (2 * n) + 1 by A2, A5, A74;

A83: ( m - 1 <= m - 0 & - 1 <= m + (- 1) ) by XREAL_1:10, XREAL_1:31;

A84: for x being object st x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } holds

card (Im (R,x)) = 1

proof

A95:
degree (Complex_of {A}) = degree (BCS (k,(Complex_of {A})))
by A11, Th32;
let x be object ; :: thesis: ( x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: card (Im (R,x)) = 1

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) 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,(Complex_of {A})) : S c= S1 } ;

A88: R .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }

card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 1 by A3, A87, Th45;

hence card (Im (R,x)) = 1 by A85, A94, RELAT_1:def 16; :: thesis: verum

end;assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: card (Im (R,x)) = 1

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) 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,(Complex_of {A})) : S c= S1 } ;

A88: R .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }

proof

{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= R .: {S}
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,(Complex_of {A})) : 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,(Complex_of {A})) : 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,(Complex_of {A})) : verum } by A46, A89;

then A91: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;

S_{2}[ss,ww]
by A46, A89;

then ( s = S & ss c= ww ) by A90, TARSKI:def 1;

hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A91; :: thesis: verum

end;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,(Complex_of {A})) : 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,(Complex_of {A})) : verum } by A46, A89;

then A91: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;

S

then ( s = S & ss c= ww ) by A90, TARSKI:def 1;

hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A91; :: thesis: verum

proof

then A94:
R .: {S} = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
by A88;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in R .: {S} )

assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in R .: {S}

then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that

A92: w = W and

A93: S c= W ;

( W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by A86;

then ( S in {S} & [S,W] in R ) by A46, A93, TARSKI:def 1;

hence w in R .: {S} by A92, RELAT_1:def 13; :: thesis: verum

end;assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in R .: {S}

then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that

A92: w = W and

A93: S c= W ;

( W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by A86;

then ( S in {S} & [S,W] in R ) by A46, A93, TARSKI:def 1;

hence w in R .: {S} by A92, RELAT_1:def 13; :: thesis: verum

card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 1 by A3, A87, Th45;

hence card (Im (R,x)) = 1 by A85, A94, RELAT_1:def 16; :: thesis: verum

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

A167:
M - 1 = m + (- 1)
by XXREAL_3:def 2;
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,(Complex_of {A})) such that

A98: x = S and

A99: Aa = F .: S ;

set FS = F | S;

A100: rng (F | S) = Aa by A99, RELAT_1:115;

A101: not Aa is empty by A5, A30;

A102: S in {x} by A98, TARSKI:def 1;

A103: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

A104: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;

reconsider FS = F | S as Function of S,Aa by A100, A103, FUNCT_2:1;

FS is onto by A100, FUNCT_2:def 3;

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 A5, A101, A104, Th2;

consider a1, a2 being object such that

A108: a1 <> a2 and

A109: FS " {b} = {a1,a2} by A106, CARD_2:60;

reconsider S1 = S \ {a1}, S2 = S \ {a2} as Simplex of (BCS (k,(Complex_of {A}))) ;

A110: a1 in {a1,a2} by TARSKI:def 2;

then A111: a1 in S2 by A108, A109, ZFMISC_1:56;

A112: card S1 = m by A104, A109, A110, STIRL2_1:55;

A113: a2 in {a1,a2} by TARSKI:def 2;

then A114: card S2 = m by A104, A109, STIRL2_1:55;

then reconsider S1 = S1, S2 = S2 as Simplex of m - 1, BCS (k,(Complex_of {A})) by A95, A83, A71, A45, A112, SIMPLEX0:def 18;

A115: {a1} c= S by A109, A110, ZFMISC_1:31;

A116: FS . a2 = F . a2 by A103, A109, A113, FUNCT_1:47;

A117: {a2} c= S by A109, A113, ZFMISC_1:31;

A118: R1 .: {x} c= {S1,S2}

A143: FS . a1 = F . a1 by A103, A109, A110, FUNCT_1:47;

A144: FS . a1 in {b} by A109, A110, FUNCT_1:def 7;

then A145: FS . a1 = b by TARSKI:def 1;

A146: FS . a2 in {b} by A109, A113, FUNCT_1:def 7;

then A147: FS . a2 = b by TARSKI:def 1;

A148: ( a2 in S & a2 in S1 ) by A108, A109, A113, ZFMISC_1:56;

A149: Aa c= F .: S1

A157: ( a1 in S & a1 in S2 ) by A108, A109, A110, ZFMISC_1:56;

A158: Aa c= F .: S2

then Aa = F .: S1 by A149;

then ( S \ {a1} c= S & S1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;

then [S,S1] in R1 by A32, A156;

then A165: S1 in R1 .: {x} by A102, RELAT_1:def 13;

F .: S2 c= Aa by A99, RELAT_1:123, XBOOLE_1:36;

then Aa = F .: S2 by A158;

then ( S \ {a2} c= S & S2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;

then [S,S2] in R1 by A32, A156;

then S2 in R1 .: {x} by A102, RELAT_1:def 13;

then {S1,S2} c= R1 .: {x} by A165, ZFMISC_1:32;

then A166: R1 .: {x} = {S1,S2} by A118;

S1 <> S2 by A111, ZFMISC_1:56;

then card (R1 .: {x}) = 2 by A166, CARD_2:57;

hence card (Im (R1,x)) = 2 by RELAT_1:def 16; :: thesis: verum

end;assume x in YA ; :: thesis: card (Im (R1,x)) = 2

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A98: x = S and

A99: Aa = F .: S ;

set FS = F | S;

A100: rng (F | S) = Aa by A99, RELAT_1:115;

A101: not Aa is empty by A5, A30;

A102: S in {x} by A98, TARSKI:def 1;

A103: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

A104: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;

reconsider FS = F | S as Function of S,Aa by A100, A103, FUNCT_2:1;

FS is onto by A100, FUNCT_2:def 3;

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 A5, A101, A104, Th2;

consider a1, a2 being object such that

A108: a1 <> a2 and

A109: FS " {b} = {a1,a2} by A106, CARD_2:60;

reconsider S1 = S \ {a1}, S2 = S \ {a2} as Simplex of (BCS (k,(Complex_of {A}))) ;

A110: a1 in {a1,a2} by TARSKI:def 2;

then A111: a1 in S2 by A108, A109, ZFMISC_1:56;

A112: card S1 = m by A104, A109, A110, STIRL2_1:55;

A113: a2 in {a1,a2} by TARSKI:def 2;

then A114: card S2 = m by A104, A109, STIRL2_1:55;

then reconsider S1 = S1, S2 = S2 as Simplex of m - 1, BCS (k,(Complex_of {A})) by A95, A83, A71, A45, A112, SIMPLEX0:def 18;

A115: {a1} c= S by A109, A110, ZFMISC_1:31;

A116: FS . a2 = F . a2 by A103, A109, A113, FUNCT_1:47;

A117: {a2} c= S by A109, A113, ZFMISC_1:31;

A118: R1 .: {x} c= {S1,S2}

proof

A142:
S c= dom F
by A18, SIMPLEX0:17;
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,(Complex_of {A})) : Aa = F .: S } by A32, A119;

then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A121: Y = W and

A122: Aa = F .: W ;

X = x by A120, TARSKI:def 1;

then S_{3}[S,W]
by A32, A98, A119, A121;

then W c= S ;

then A123: Aa = FS .: W by A122, RELAT_1:129;

then consider w being object such that

A124: w in dom FS and

A125: w in W and

A126: FS . w = b by A105, FUNCT_1:def 6;

A127: {w} c= W by A125, ZFMISC_1:31;

A128: S \ {a1,a2} c= W

then A138: w in FS " {b} by A124, A126, FUNCT_1:def 7;

A139: card W = m by A95, A83, A71, A45, SIMPLEX0:def 18;

A140: S /\ {a1} = {a1} by A115, XBOOLE_1:28;

A141: S /\ {a2} = {a2} by A117, XBOOLE_1:28;

end;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,(Complex_of {A})) : Aa = F .: S } by A32, A119;

then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A121: Y = W and

A122: Aa = F .: W ;

X = x by A120, TARSKI:def 1;

then S

then W c= S ;

then A123: Aa = FS .: W by A122, RELAT_1:129;

then consider w being object such that

A124: w in dom FS and

A125: w in W and

A126: FS . w = b by A105, FUNCT_1:def 6;

A127: {w} c= W by A125, ZFMISC_1:31;

A128: S \ {a1,a2} c= W

proof

b in {b}
by TARSKI:def 1;
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 A103, XBOOLE_0:def 5;

then A131: FS . s in Aa by A100, FUNCT_1:def 3;

then consider w being object such that

A132: w in dom FS and

A133: w in W and

A134: FS . w = FS . s by A123, FUNCT_1:def 6;

not s in FS " {b} by A109, A129, XBOOLE_0:def 5;

then not FS . s in {b} by A130, FUNCT_1:def 7;

then FS . s <> b by TARSKI:def 1;

then card (FS " {(FS . s)}) = 1 by A107, A131;

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 A130, FUNCT_1:def 7;

w in FS " {(FS . s)} by A132, A134, A136, FUNCT_1:def 7;

then w = z by A135, TARSKI:def 1;

hence s in W by A133, A135, A137, TARSKI:def 1; :: thesis: verum

end;assume A129: s in S \ {a1,a2} ; :: thesis: s in W

then A130: s in dom FS by A103, XBOOLE_0:def 5;

then A131: FS . s in Aa by A100, FUNCT_1:def 3;

then consider w being object such that

A132: w in dom FS and

A133: w in W and

A134: FS . w = FS . s by A123, FUNCT_1:def 6;

not s in FS " {b} by A109, A129, XBOOLE_0:def 5;

then not FS . s in {b} by A130, FUNCT_1:def 7;

then FS . s <> b by TARSKI:def 1;

then card (FS " {(FS . s)}) = 1 by A107, A131;

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 A130, FUNCT_1:def 7;

w in FS " {(FS . s)} by A132, A134, A136, FUNCT_1:def 7;

then w = z by A135, TARSKI:def 1;

hence s in W by A133, A135, A137, TARSKI:def 1; :: thesis: verum

then A138: w in FS " {b} by A124, A126, FUNCT_1:def 7;

A139: card W = m by A95, A83, A71, A45, SIMPLEX0:def 18;

A140: S /\ {a1} = {a1} by A115, XBOOLE_1:28;

A141: S /\ {a2} = {a2} by A117, XBOOLE_1:28;

per cases
( w = a1 or w = a2 )
by A109, A138, TARSKI:def 2;

end;

A143: FS . a1 = F . a1 by A103, A109, A110, FUNCT_1:47;

A144: FS . a1 in {b} by A109, A110, FUNCT_1:def 7;

then A145: FS . a1 = b by TARSKI:def 1;

A146: FS . a2 in {b} by A109, A113, FUNCT_1:def 7;

then A147: FS . a2 = b by TARSKI:def 1;

A148: ( a2 in S & a2 in S1 ) by A108, A109, A113, ZFMISC_1:56;

A149: Aa c= F .: S1

proof

A156:
S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
;
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

end;assume A150: z in Aa ; :: thesis: z in F .: S1

A157: ( a1 in S & a1 in S2 ) by A108, A109, A110, ZFMISC_1:56;

A158: Aa c= F .: S2

proof

F .: S1 c= Aa
by A99, RELAT_1:123, XBOOLE_1:36;
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

end;assume A159: z in Aa ; :: thesis: z in F .: S2

then Aa = F .: S1 by A149;

then ( S \ {a1} c= S & S1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;

then [S,S1] in R1 by A32, A156;

then A165: S1 in R1 .: {x} by A102, RELAT_1:def 13;

F .: S2 c= Aa by A99, RELAT_1:123, XBOOLE_1:36;

then Aa = F .: S2 by A158;

then ( S \ {a2} c= S & S2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;

then [S,S2] in R1 by A32, A156;

then S2 in R1 .: {x} by A102, RELAT_1:def 13;

then {S1,S2} c= R1 .: {x} by A165, ZFMISC_1:32;

then A166: R1 .: {x} = {S1,S2} by A118;

S1 <> S2 by A111, ZFMISC_1:56;

then card (R1 .: {x}) = 2 by A166, CARD_2:57;

hence card (Im (R1,x)) = 2 by RELAT_1:def 16; :: thesis: verum

XX c= (dom R1) \ YA

proof

then A179:
(dom R1) \ YA = XX
by A33;
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,(Complex_of {A})) such that

A168: x = S and

A169: F .: S = A by A3;

set FS = F | S;

A170: rng (F | S) = A by A169, RELAT_1:115;

A171: card A = card S by A3, A95, A45, A96, SIMPLEX0:def 18;

A172: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

then reconsider FS = F | S as Function of S,A by A170, FUNCT_2:1;

consider s being object such that

A173: ( s in dom FS & FS . s = a ) by A4, A170, FUNCT_1:def 3;

set Ss = S \ {s};

FS is onto by A170, FUNCT_2:def 3;

then A174: FS is one-to-one by A171, STIRL2_1:60;

then A175: FS .: (S \ {s}) = (FS .: S) \ (FS .: {s}) by FUNCT_1:64

.= A \ (FS .: {s}) by A170, A172, RELAT_1:113

.= A \ (Im (FS,s)) by RELAT_1:def 16

.= Aa by A173, FUNCT_1:59 ;

S \ {s},FS .: (S \ {s}) are_equipotent by A172, A174, CARD_1:33, XBOOLE_1:36;

then A176: card (S \ {s}) = m by A5, A175, CARD_1:5;

reconsider Ss = S \ {s} as Simplex of (BCS (k,(Complex_of {A}))) ;

reconsider Ss = Ss as Simplex of m - 1, BCS (k,(Complex_of {A})) by A167, A176, SIMPLEX0:48;

FS .: Ss = F .: Ss by RELAT_1:129, XBOOLE_1:36;

then A177: Ss in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A175;

( Ss c= S & S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ) by XBOOLE_1:36;

then [S,Ss] in R1 by A32, A177;

then A178: S in dom R1 by XTUPLE_0:def 12;

for W being Simplex of m, BCS (k,(Complex_of {A})) st S = W holds

Aa <> F .: W by A4, A169, ZFMISC_1:56;

then not S in YA ;

hence x in (dom R1) \ YA by A168, A178, XBOOLE_0:def 5; :: thesis: verum

end;assume x in XX ; :: thesis: x in (dom R1) \ YA

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A168: x = S and

A169: F .: S = A by A3;

set FS = F | S;

A170: rng (F | S) = A by A169, RELAT_1:115;

A171: card A = card S by A3, A95, A45, A96, SIMPLEX0:def 18;

A172: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

then reconsider FS = F | S as Function of S,A by A170, FUNCT_2:1;

consider s being object such that

A173: ( s in dom FS & FS . s = a ) by A4, A170, FUNCT_1:def 3;

set Ss = S \ {s};

FS is onto by A170, FUNCT_2:def 3;

then A174: FS is one-to-one by A171, STIRL2_1:60;

then A175: FS .: (S \ {s}) = (FS .: S) \ (FS .: {s}) by FUNCT_1:64

.= A \ (FS .: {s}) by A170, A172, RELAT_1:113

.= A \ (Im (FS,s)) by RELAT_1:def 16

.= Aa by A173, FUNCT_1:59 ;

S \ {s},FS .: (S \ {s}) are_equipotent by A172, A174, CARD_1:33, XBOOLE_1:36;

then A176: card (S \ {s}) = m by A5, A175, CARD_1:5;

reconsider Ss = S \ {s} as Simplex of (BCS (k,(Complex_of {A}))) ;

reconsider Ss = Ss as Simplex of m - 1, BCS (k,(Complex_of {A})) by A167, A176, SIMPLEX0:48;

FS .: Ss = F .: Ss by RELAT_1:129, XBOOLE_1:36;

then A177: Ss in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A175;

( Ss c= S & S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ) by XBOOLE_1:36;

then [S,Ss] in R1 by A32, A177;

then A178: S in dom R1 by XTUPLE_0:def 12;

for W being Simplex of m, BCS (k,(Complex_of {A})) st S = W holds

Aa <> F .: W by A4, A169, ZFMISC_1:56;

then not S in YA ;

hence x in (dom R1) \ YA by A168, A178, XBOOLE_0:def 5; :: thesis: verum

for x being object st x in (dom R1) \ YA holds

card (Im ((R1 | ((dom R1) \ YA)),x)) = 1

proof

then card (R1 | ((dom R1) \ YA)) =
(card {}) +` (1 *` (card ((dom R1) \ YA)))
by A40, Th1
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,(Complex_of {A})) st

( x = W & F .: W = A ) by A3, A179, A180;

x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A32, A181;

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A183: x = S and

verum ;

y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A181;

then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A184: y = W and

A185: Aa = F .: W ;

A186: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;

A187: (R1 | ((dom R1) \ YA)) .: {x} c= {y}

then y in (R1 | ((dom R1) \ YA)) .: {x} by RELAT_1:def 13;

then (R1 | ((dom R1) \ YA)) .: {x} = {y} by A187, ZFMISC_1:33;

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;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,(Complex_of {A})) st

( x = W & F .: W = A ) by A3, A179, A180;

x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A32, A181;

then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that

A183: x = S and

verum ;

y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A181;

then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A184: y = W and

A185: Aa = F .: W ;

A186: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;

A187: (R1 | ((dom R1) \ YA)) .: {x} c= {y}

proof

( x in {x} & [x,y] in R1 | ((dom R1) \ YA) )
by A180, A181, RELAT_1:def 11, TARSKI:def 1;
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 A188, RELAT_1:def 11;

then u in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32;

then consider U being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A191: u = U and

A192: Aa = F .: U ;

A193: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

A194: rng (F | S) = A by A182, A183, RELAT_1:115;

then reconsider FS = F | S as Function of S,A by A193, FUNCT_2:1;

S_{3}[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 A183, A189, TARSKI:def 1;

then S_{3}[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 A194, FUNCT_2:def 3;

then A199: FS is one-to-one by A3, A186, STIRL2_1:60;

then A200: U c= W by A185, A192, A193, A196, A197, A198, FUNCT_1:87;

W c= U by A185, A192, A193, A195, A196, A198, A199, FUNCT_1:87;

then u = y by A184, A191, A200, XBOOLE_0:def 10;

hence u in {y} by TARSKI:def 1; :: thesis: verum

end;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 A188, RELAT_1:def 11;

then u in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32;

then consider U being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A191: u = U and

A192: Aa = F .: U ;

A193: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;

A194: rng (F | S) = A by A182, A183, RELAT_1:115;

then reconsider FS = F | S as Function of S,A by A193, FUNCT_2:1;

S

then A195: W c= S ;

then A196: FS .: W = F .: W by RELAT_1:129;

s = S by A183, A189, TARSKI:def 1;

then S

then A197: U c= S ;

then A198: FS .: U = F .: U by RELAT_1:129;

FS is onto by A194, FUNCT_2:def 3;

then A199: FS is one-to-one by A3, A186, STIRL2_1:60;

then A200: U c= W by A185, A192, A193, A196, A197, A198, FUNCT_1:87;

W c= U by A185, A192, A193, A195, A196, A198, A199, FUNCT_1:87;

then u = y by A184, A191, A200, XBOOLE_0:def 10;

hence u in {y} by TARSKI:def 1; :: thesis: verum

then y in (R1 | ((dom R1) \ YA)) .: {x} by RELAT_1:def 13;

then (R1 | ((dom R1) \ YA)) .: {x} = {y} by A187, ZFMISC_1:33;

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

.= 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 A44, A97, A179, Th1

.= card ((card XX) + (2 * (card YA))) by CARD_2:38

.= (card XX) + (2 * (card YA)) ;

A202: ( |.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| & |.(Complex_of {A}).| = conv A ) by Th8, Th10;

A203: { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }

proof

A223:
degree (Complex_of {Aa}) = m - 1
by A5, A167, SIMPLEX0:26;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } )

assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A204: x = S and

A205: F .: S = Aa and

A206: conv (@ S) misses Int A ;

conv (@ S) c= conv A by A202, Th5;

then consider B being Subset of V such that

A207: B c< A and

A208: conv (@ S) c= conv B by A4, A206, RLAFFIN2:23;

A209: B c= A by A207;

then reconsider B = B as finite Subset of V ;

card B < m + 1 by A3, A207, CARD_2:48;

then A210: card B <= m by NAT_1:13;

A211: Aa c= B

then A215: Aa = B by A5, A210, A211, CARD_2:102, XXREAL_0:1;

A216: the topology of (BCS (k,(Complex_of {Aa}))) c= the topology of (BCS (k,(Complex_of {A}))) by A14, SIMPLEX0:def 13;

A217: card S = m by A95, A83, A71, A45, SIMPLEX0:def 18;

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,(Complex_of {Aa}))) such that

A219: w is simplex-like and

A220: (center_of_mass V) . S in conv (@ w) by A65, A208, A215, Def3;

w in the topology of (BCS (k,(Complex_of {Aa}))) by A219;

then w in the topology of (BCS (k,(Complex_of {A}))) by A216;

then reconsider W = w as Simplex of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2;

Int (@ S) meets conv (@ W) by A218, A220, XBOOLE_0:3;

then A221: S c= w by Th26;

then reconsider s = S as Subset of (BCS (k,(Complex_of {Aa}))) by XBOOLE_1:1;

reconsider s = s as Simplex of (BCS (k,(Complex_of {Aa}))) by A219, A221, MATROID0:1;

A222: FA .: s = Aa by A205, RELAT_1:129, SIMPLEX0:17;

s is Simplex of m - 1, BCS (k,(Complex_of {Aa})) by A167, A217, SIMPLEX0:48;

hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } by A204, A222; :: thesis: verum

end;assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A204: x = S and

A205: F .: S = Aa and

A206: conv (@ S) misses Int A ;

conv (@ S) c= conv A by A202, Th5;

then consider B being Subset of V such that

A207: B c< A and

A208: conv (@ S) c= conv B by A4, A206, RLAFFIN2:23;

A209: B c= A by A207;

then reconsider B = B as finite Subset of V ;

card B < m + 1 by A3, A207, CARD_2:48;

then A210: card B <= m by NAT_1:13;

A211: Aa c= B

proof

then
card Aa <= card B
by NAT_1:43;
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 A205, FUNCT_1:def 6;

S c= conv (@ S) by RLAFFIN1:2;

then v in conv (@ S) by A213;

hence y in B by A9, A208, A209, A212, A214; :: thesis: verum

end;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 A205, FUNCT_1:def 6;

S c= conv (@ S) by RLAFFIN1:2;

then v in conv (@ S) by A213;

hence y in B by A9, A208, A209, A212, A214; :: thesis: verum

then A215: Aa = B by A5, A210, A211, CARD_2:102, XXREAL_0:1;

A216: the topology of (BCS (k,(Complex_of {Aa}))) c= the topology of (BCS (k,(Complex_of {A}))) by A14, SIMPLEX0:def 13;

A217: card S = m by A95, A83, A71, A45, SIMPLEX0:def 18;

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,(Complex_of {Aa}))) such that

A219: w is simplex-like and

A220: (center_of_mass V) . S in conv (@ w) by A65, A208, A215, Def3;

w in the topology of (BCS (k,(Complex_of {Aa}))) by A219;

then w in the topology of (BCS (k,(Complex_of {A}))) by A216;

then reconsider W = w as Simplex of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2;

Int (@ S) meets conv (@ W) by A218, A220, XBOOLE_0:3;

then A221: S c= w by Th26;

then reconsider s = S as Subset of (BCS (k,(Complex_of {Aa}))) by XBOOLE_1:1;

reconsider s = s as Simplex of (BCS (k,(Complex_of {Aa}))) by A219, A221, MATROID0:1;

A222: FA .: s = Aa by A205, RELAT_1:129, SIMPLEX0:17;

s is Simplex of m - 1, BCS (k,(Complex_of {Aa})) by A167, A217, SIMPLEX0:48;

hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } by A204, A222; :: thesis: verum

{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }

proof

then A228:
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
by A203;
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,(Complex_of {Aa})) : FA .: S = Aa } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )

assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }

then consider S being Simplex of m - 1, BCS (k,(Complex_of {Aa})) such that

A225: x = S and

A226: FA .: S = Aa ;

m - 1 <= degree (BCS (k,(Complex_of {Aa}))) by A7, A223, Th32;

then reconsider S1 = x as Simplex of m - 1, BCS (k,(Complex_of {A})) by A14, A225, SIMPLEX0:49;

A227: FA .: S = F .: S by RELAT_1:129, SIMPLEX0:17;

conv (@ S) c= conv Aa by A65, Th5;

then conv (@ S1) misses Int A by A224, A225, RLAFFIN2:7, XBOOLE_1:63;

hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A225, A226, A227; :: thesis: verum

end;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,(Complex_of {Aa})) : FA .: S = Aa } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )

assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }

then consider S being Simplex of m - 1, BCS (k,(Complex_of {Aa})) such that

A225: x = S and

A226: FA .: S = Aa ;

m - 1 <= degree (BCS (k,(Complex_of {Aa}))) by A7, A223, Th32;

then reconsider S1 = x as Simplex of m - 1, BCS (k,(Complex_of {A})) by A14, A225, SIMPLEX0:49;

A227: FA .: S = F .: S by RELAT_1:129, SIMPLEX0:17;

conv (@ S) c= conv Aa by A65, Th5;

then conv (@ S1) misses Int A by A224, A225, RLAFFIN2:7, XBOOLE_1:63;

hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A225, A226, A227; :: thesis: verum

for x being object st x in DX holds

card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2

proof

then card (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) =
(card ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX))) +` (2 *` (card DX))
by Th1
let x be object ; :: thesis: ( x in DX implies card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : ( 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,(Complex_of {A})) : Aa = F .: S } by A46;

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A231: x = S and

A232: Aa = F .: S ;

set XX = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;

not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A229, XBOOLE_0:def 5;

then conv (@ S) meets Int A by A231, A232;

then A233: card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 2 by A3, Th45;

A234: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }

hence card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 by A231, A233, RELAT_1:def 16; :: thesis: verum

end;assume A229: x in DX ; :: thesis: card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( 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,(Complex_of {A})) : Aa = F .: S } by A46;

then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that

A231: x = S and

A232: Aa = F .: S ;

set XX = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;

not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A229, XBOOLE_0:def 5;

then conv (@ S) meets Int A by A231, A232;

then A233: card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 2 by A3, Th45;

A234: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }

proof

{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) and

A236: s in {S} by RELAT_1:def 13;

A237: [s,w] in R by A235, RELAT_1:def 11;

then w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A46;

then A238: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;

s = S by A236, TARSKI:def 1;

then S_{2}[S,ww]
by A46, A237;

then S c= ww ;

hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A238; :: thesis: verum

end;reconsider ww = w as set by TARSKI:1;

assume w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) and

A236: s in {S} by RELAT_1:def 13;

A237: [s,w] in R by A235, RELAT_1:def 11;

then w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A46;

then A238: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;

s = S by A236, TARSKI:def 1;

then S

then S c= ww ;

hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A238; :: thesis: verum

proof

then
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
by A234;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} )

assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}

then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that

A239: w = W and

A240: S c= W ;

W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;

then [S,W] in R by A46, A230, A231, A240;

then A241: [S,W] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) by A229, A231, RELAT_1:def 11;

S in {S} by TARSKI:def 1;

hence w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by A239, A241, RELAT_1:def 13; :: thesis: verum

end;assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}

then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that

A239: w = W and

A240: S c= W ;

W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;

then [S,W] in R by A46, A230, A231, A240;

then A241: [S,W] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) by A229, A231, RELAT_1:def 11;

S in {S} by TARSKI:def 1;

hence w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by A239, A241, RELAT_1:def 13; :: thesis: verum

hence card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 by A231, A233, RELAT_1:def 16; :: thesis: verum

.= 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,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) by A84, Th1

.= (2 *` (card DX)) +` ((2 * n) + 1) by A82, A228, CARD_2:21

.= ((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 A47, A201;

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,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1

thus card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1 by A47, A201, A242; :: thesis: verum

proof

for k being Nat holds S
let A be finite affinely-independent Subset of V; :: thesis: ( card A = 0 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A244: card A = 0 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

A245: A = {} by A244;

set C = Complex_of {A};

A246: ( |.(Complex_of {A}).| c= [#] V & [#] (Complex_of {A}) = [#] V ) ;

let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

set X = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;

take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1

A247: ( k = 0 or k > 0 ) ;

A248: Z - 1 = - 1 by XXREAL_3:4;

then degree (Complex_of {A}) = - 1 by A244, SIMPLEX0:26;

then A249: Complex_of {A} = BCS (k,(Complex_of {A})) by A246, A247, Th16, Th22;

A250: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;

A251: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= {A}

then reconsider A1 = A as Simplex of (Complex_of {A}) by A250, PRE_TOPC:def 2;

A254: F .: A1 = A by A245;

A1 is Simplex of - 1, Complex_of {A} by A244, A248, SIMPLEX0:48;

then A in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } by A249, A254;

then { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = {A} by A251, ZFMISC_1:33;

hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum

end;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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume A244: card A = 0 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

A245: A = {} by A244;

set C = Complex_of {A};

A246: ( |.(Complex_of {A}).| c= [#] V & [#] (Complex_of {A}) = [#] V ) ;

let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )

assume for v being Vertex of (BCS (k,(Complex_of {A})))

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,(Complex_of {A})) : F .: S = A } = (2 * n) + 1

set X = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;

take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1

A247: ( k = 0 or k > 0 ) ;

A248: Z - 1 = - 1 by XXREAL_3:4;

then degree (Complex_of {A}) = - 1 by A244, SIMPLEX0:26;

then A249: Complex_of {A} = BCS (k,(Complex_of {A})) by A246, A247, Th16, Th22;

A250: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;

A251: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= {A}

proof

A in bool A
by ZFMISC_1:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } or x in {A} )

assume A252: x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in {A}

consider S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) such that

A253: S = x and

F .: S = A by A252;

S in the topology of (Complex_of {A}) by A249, PRE_TOPC:def 2;

then S is empty by A245, A250;

hence x in {A} by A245, A253, TARSKI:def 1; :: thesis: verum

end;assume A252: x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in {A}

consider S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) such that

A253: S = x and

F .: S = A by A252;

S in the topology of (Complex_of {A}) by A249, PRE_TOPC:def 2;

then S is empty by A245, A250;

hence x in {A} by A245, A253, TARSKI:def 1; :: thesis: verum

then reconsider A1 = A as Simplex of (Complex_of {A}) by A250, PRE_TOPC:def 2;

A254: F .: A1 = A by A245;

A1 is Simplex of - 1, Complex_of {A} by A244, A248, SIMPLEX0:48;

then A in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } by A249, A254;

then { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = {A} by A251, ZFMISC_1:33;

hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum

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