let n be Nat; :: thesis: for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let A be finite Subset of V; :: thesis: ( K is Subdivision of Complex_of {A} & card A = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) ) implies for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) )

assume that

A1: K is Subdivision of Complex_of {A} and

A2: card A = n + 1 and

A3: degree K = n and

A4: for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) ; :: thesis: for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

|.(Complex_of {A}).| = conv A by Th8;

then A5: |.K.| = conv A by A1, Th10;

A6: K is finite-degree by A3, SIMPLEX0:def 12;

A7: A is affinely-independent

reconsider Z = 0 as Nat ;

set TK = TopStruct(# the carrier of K, the topology of K #);

reconsider n1 = n - 1 as ExtReal ;

let S be Simplex of n - 1, BCS K; :: thesis: for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

let X be set ; :: thesis: ( X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } implies ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) )

assume A11: X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } ; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

[#] K = the carrier of V by SIMPLEX0:def 10;

then A12: |.K.| c= [#] K ;

then A13: degree K = degree (BCS K) by Th31;

then A14: ( n + (- 1) >= - 1 & n - 1 <= degree (BCS K) ) by A3, XREAL_1:31, XREAL_1:146;

then A15: card S = n1 + 1 by SIMPLEX0:def 18;

then A16: card S = (n - 1) + 1 by XXREAL_3:def 2;

A17: BCS K = subdivision ((center_of_mass V),K) by A12, Def5;

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Af being finite Subset of V st K is Subdivision of Complex_of {Af} & card Af = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds

for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int Af implies card X = 2 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )

let A be finite Subset of V; :: thesis: ( K is Subdivision of Complex_of {A} & card A = n + 1 & degree K = n & ( for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) ) implies for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) )

assume that

A1: K is Subdivision of Complex_of {A} and

A2: card A = n + 1 and

A3: degree K = n and

A4: for S being Simplex of n - 1,K

for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) ; :: thesis: for S being Simplex of n - 1, BCS K

for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

|.(Complex_of {A}).| = conv A by Th8;

then A5: |.K.| = conv A by A1, Th10;

A6: K is finite-degree by A3, SIMPLEX0:def 12;

A7: A is affinely-independent

proof

set B = center_of_mass V;
consider a being Subset of K such that

A8: a is simplex-like and

A9: card a = (degree K) + 1 by A6, SIMPLEX0:def 12;

conv (@ a) c= conv A by A5, A8, Th5;

then A10: Affin (@ a) c= Affin A by RLAFFIN1:68;

card A = card a by A2, A3, A9, XXREAL_3:def 2;

hence A is affinely-independent by A8, A10, RLAFFIN1:80; :: thesis: verum

end;A8: a is simplex-like and

A9: card a = (degree K) + 1 by A6, SIMPLEX0:def 12;

conv (@ a) c= conv A by A5, A8, Th5;

then A10: Affin (@ a) c= Affin A by RLAFFIN1:68;

card A = card a by A2, A3, A9, XXREAL_3:def 2;

hence A is affinely-independent by A8, A10, RLAFFIN1:80; :: thesis: verum

reconsider Z = 0 as Nat ;

set TK = TopStruct(# the carrier of K, the topology of K #);

reconsider n1 = n - 1 as ExtReal ;

let S be Simplex of n - 1, BCS K; :: thesis: for X being set st X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } holds

( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

let X be set ; :: thesis: ( X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } implies ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) )

assume A11: X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } ; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

[#] K = the carrier of V by SIMPLEX0:def 10;

then A12: |.K.| c= [#] K ;

then A13: degree K = degree (BCS K) by Th31;

then A14: ( n + (- 1) >= - 1 & n - 1 <= degree (BCS K) ) by A3, XREAL_1:31, XREAL_1:146;

then A15: card S = n1 + 1 by SIMPLEX0:def 18;

then A16: card S = (n - 1) + 1 by XXREAL_3:def 2;

A17: BCS K = subdivision ((center_of_mass V),K) by A12, Def5;

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

end;

suppose A18:
n = 0
; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

then A19:
TopStruct(# the carrier of K, the topology of K #) = BCS K
by A3, A12, Th21;

then S in the topology of K by PRE_TOPC:def 2;

then reconsider s = S as Simplex of K by PRE_TOPC:def 2;

reconsider s = s as Simplex of n - 1,K by A3, A15, A18, SIMPLEX0:def 18;

set XX = { W where W is Simplex of n,K : s c= W } ;

A20: @ S = @ s ;

then A21: ( conv (@ S) meets Int A implies card { W where W is Simplex of n,K : s c= W } = 2 ) by A4;

A22: { W where W is Simplex of n,K : s c= W } c= X

hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A22, A24, A21, XBOOLE_0:def 10; :: thesis: verum

end;then S in the topology of K by PRE_TOPC:def 2;

then reconsider s = S as Simplex of K by PRE_TOPC:def 2;

reconsider s = s as Simplex of n - 1,K by A3, A15, A18, SIMPLEX0:def 18;

set XX = { W where W is Simplex of n,K : s c= W } ;

A20: @ S = @ s ;

then A21: ( conv (@ S) meets Int A implies card { W where W is Simplex of n,K : s c= W } = 2 ) by A4;

A22: { W where W is Simplex of n,K : s c= W } c= X

proof

A24:
X c= { W where W is Simplex of n,K : s c= W }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Simplex of n,K : s c= W } or x in X )

assume x in { W where W is Simplex of n,K : s c= W } ; :: thesis: x in X

then consider W being Simplex of n,K such that

A23: ( x = W & S c= W ) ;

W in the topology of (BCS K) by A19, PRE_TOPC:def 2;

then reconsider w = W as Simplex of (BCS K) by PRE_TOPC:def 2;

card W = (degree K) + 1 by A3, SIMPLEX0:def 18;

then w is Simplex of n, BCS K by A3, A13, SIMPLEX0:def 18;

hence x in X by A11, A23; :: thesis: verum

end;assume x in { W where W is Simplex of n,K : s c= W } ; :: thesis: x in X

then consider W being Simplex of n,K such that

A23: ( x = W & S c= W ) ;

W in the topology of (BCS K) by A19, PRE_TOPC:def 2;

then reconsider w = W as Simplex of (BCS K) by PRE_TOPC:def 2;

card W = (degree K) + 1 by A3, SIMPLEX0:def 18;

then w is Simplex of n, BCS K by A3, A13, SIMPLEX0:def 18;

hence x in X by A11, A23; :: thesis: verum

proof

( conv (@ S) misses Int A implies card { W where W is Simplex of n,K : s c= W } = 1 )
by A4, A20;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { W where W is Simplex of n,K : s c= W } )

assume x in X ; :: thesis: x in { W where W is Simplex of n,K : s c= W }

then consider W being Simplex of n, BCS K such that

A25: ( x = W & S c= W ) by A11;

W in the topology of K by A19, PRE_TOPC:def 2;

then reconsider w = W as Simplex of K by PRE_TOPC:def 2;

card W = (degree (BCS K)) + 1 by A3, A13, SIMPLEX0:def 18;

then w is Simplex of n,K by A3, A13, SIMPLEX0:def 18;

hence x in { W where W is Simplex of n,K : s c= W } by A25; :: thesis: verum

end;assume x in X ; :: thesis: x in { W where W is Simplex of n,K : s c= W }

then consider W being Simplex of n, BCS K such that

A25: ( x = W & S c= W ) by A11;

W in the topology of K by A19, PRE_TOPC:def 2;

then reconsider w = W as Simplex of K by PRE_TOPC:def 2;

card W = (degree (BCS K)) + 1 by A3, A13, SIMPLEX0:def 18;

then w is Simplex of n,K by A3, A13, SIMPLEX0:def 18;

hence x in { W where W is Simplex of n,K : s c= W } by A25; :: thesis: verum

hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A22, A24, A21, XBOOLE_0:def 10; :: thesis: verum

suppose A26:
n > 0
; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

consider SS being c=-linear finite simplex-like Subset-Family of K such that

A27: S = (center_of_mass V) .: SS by A17, SIMPLEX0:def 20;

SS \ {{}} c= SS by XBOOLE_1:36;

then reconsider SS1 = SS \ {{}} as c=-linear finite simplex-like Subset-Family of K by TOPS_2:11;

A28: ( SS1 c= bool (@ (union SS1)) & bool (@ (union SS1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

A29: not {} in SS1 by ZFMISC_1:56;

then A30: SS1 is with_non-empty_elements ;

A31: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

then A32: SS /\ (dom (center_of_mass V)) = (SS /\ (bool the carrier of V)) \ {{}} by XBOOLE_1:49

.= SS1 /\ (bool the carrier of V) by XBOOLE_1:49

.= SS1 by A28, XBOOLE_1:1, XBOOLE_1:28 ;

then A33: (center_of_mass V) .: SS = (center_of_mass V) .: SS1 by RELAT_1:112;

then A34: card SS1 = n by A16, A27, A30, Th33;

A35: S = (center_of_mass V) .: SS1 by A27, A32, RELAT_1:112;

A36: card SS1 = card S by A27, A30, A33, Th33;

then A37: not SS1 is empty by A16, A26;

then A38: union SS1 in SS1 by SIMPLEX0:9;

then reconsider U = union SS1 as Simplex of K by TOPS_2:def 1;

Segm (card SS1) c= Segm (card U) by A30, SIMPLEX0:10;

then A39: n <= card U by A16, A36, NAT_1:39;

card U <= (degree K) + 1 by SIMPLEX0:24;

then A40: card U <= n + 1 by A3, XXREAL_3:def 2;

A41: conv (@ U) c= conv A by A5, Th5;

SS1 c= bool the carrier of V by A28;

then A42: conv (@ S) c= conv (@ U) by A35, CONVEX1:30, RLAFFIN2:17;

end;A27: S = (center_of_mass V) .: SS by A17, SIMPLEX0:def 20;

SS \ {{}} c= SS by XBOOLE_1:36;

then reconsider SS1 = SS \ {{}} as c=-linear finite simplex-like Subset-Family of K by TOPS_2:11;

A28: ( SS1 c= bool (@ (union SS1)) & bool (@ (union SS1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

A29: not {} in SS1 by ZFMISC_1:56;

then A30: SS1 is with_non-empty_elements ;

A31: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

then A32: SS /\ (dom (center_of_mass V)) = (SS /\ (bool the carrier of V)) \ {{}} by XBOOLE_1:49

.= SS1 /\ (bool the carrier of V) by XBOOLE_1:49

.= SS1 by A28, XBOOLE_1:1, XBOOLE_1:28 ;

then A33: (center_of_mass V) .: SS = (center_of_mass V) .: SS1 by RELAT_1:112;

then A34: card SS1 = n by A16, A27, A30, Th33;

A35: S = (center_of_mass V) .: SS1 by A27, A32, RELAT_1:112;

A36: card SS1 = card S by A27, A30, A33, Th33;

then A37: not SS1 is empty by A16, A26;

then A38: union SS1 in SS1 by SIMPLEX0:9;

then reconsider U = union SS1 as Simplex of K by TOPS_2:def 1;

Segm (card SS1) c= Segm (card U) by A30, SIMPLEX0:10;

then A39: n <= card U by A16, A36, NAT_1:39;

card U <= (degree K) + 1 by SIMPLEX0:24;

then A40: card U <= n + 1 by A3, XXREAL_3:def 2;

A41: conv (@ U) c= conv A by A5, Th5;

SS1 c= bool the carrier of V by A28;

then A42: conv (@ S) c= conv (@ U) by A35, CONVEX1:30, RLAFFIN2:17;

per cases
( card U = n or card U = n + 1 )
by A39, A40, NAT_1:9;

end;

suppose A43:
card U = n
; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

set XX = { W where W is Simplex of n,K : U c= W } ;

A44: U is Simplex of n - 1,K by A13, A14, A15, A16, A43, SIMPLEX0:def 18;

assume conv (@ S) misses Int A ; :: thesis: card X = 1

then consider BB being Subset of V such that

A79: BB c< A and

A80: conv (@ S) c= conv BB by A7, A78, RLAFFIN2:23;

A81: BB c= A by A79;

then reconsider B1 = BB as finite Subset of V ;

card B1 < n + 1 by A2, A79, CARD_2:48;

then A82: card B1 <= n by NAT_1:13;

Affin (@ S) c= Affin BB by A80, RLAFFIN1:68;

then n <= card B1 by A16, RLAFFIN1:79;

then card B1 = n by A82, XXREAL_0:1;

then card (A \ BB) = (n + 1) - n by A2, A81, CARD_2:44;

then consider ab being object such that

A83: A \ BB = {ab} by CARD_2:42;

not U is empty by A26, A43;

then @ U in dom (center_of_mass V) by A31, ZFMISC_1:56;

then A84: ( S c= conv (@ S) & (center_of_mass V) . U in @ S ) by A35, A38, FUNCT_1:def 6, RLAFFIN1:2;

then (center_of_mass V) . U in conv (@ S) ;

then A85: (center_of_mass V) . U in conv (@ U) by A42;

set BUU = ((center_of_mass V) . U) |-- (@ U);

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

then A86: @ U c= conv A by A41;

A87: ab in {ab} by TARSKI:def 1;

then reconsider ab = ab as Element of V by A83;

A88: ( SS1 is with_non-empty_elements & S = (center_of_mass V) .: SS1 ) by A27, A29, A32, RELAT_1:112;

A89: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;

then sum (((center_of_mass V) . U) |-- (@ U)) = 1 by A85, RLAFFIN1:def 7;

then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that

A90: ((Sum (((center_of_mass V) . U) |-- (@ U))) |-- A) . ab = Sum F and

A91: len G = len F and

G is one-to-one and

A92: rng G = Carrier (((center_of_mass V) . U) |-- (@ U)) and

A93: for n being Nat st n in dom F holds

F . n = ((((center_of_mass V) . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by A7, A86, RLAFFIN2:3;

A94: dom G = dom F by A91, FINSEQ_3:29;

U c= conv B1

then conv (@ U) misses Int A by A79, RLAFFIN2:7, XBOOLE_1:63;

then card { W where W is Simplex of n,K : U c= W } = 1 by A4, A44;

then consider w1 being object such that

A112: { W where W is Simplex of n,K : U c= W } = {w1} by CARD_2:42;

w1 in { W where W is Simplex of n,K : U c= W } by A112, TARSKI:def 1;

then consider W1 being Simplex of n,K such that

A113: w1 = W1 and

A114: U c= W1 ;

A115: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;

A116: X c= {(S \/ ((center_of_mass V) .: {W1}))}

then card W1 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A114, Th42;

then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;

then ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;

then S \/ ((center_of_mass V) .: {W1}) in X by A11;

then X = {(S \/ ((center_of_mass V) .: {W1}))} by A116, ZFMISC_1:33;

hence card X = 1 by CARD_1:30; :: thesis: verum

end;A44: U is Simplex of n - 1,K by A13, A14, A15, A16, A43, SIMPLEX0:def 18;

hereby :: thesis: ( conv (@ S) misses Int A implies card X = 1 )

A78:
( conv (@ S) c= conv A & not A is empty )
by A2, A41, A42;assume
conv (@ S) meets Int A
; :: thesis: card X = 2

then conv (@ U) meets Int A by A42, XBOOLE_1:63;

then A45: card { W where W is Simplex of n,K : U c= W } = 2 by A4, A44;

consider w1, w2 being object such that

A46: w1 <> w2 and

A47: { W where W is Simplex of n,K : U c= W } = {w1,w2} by A45, CARD_2:60;

w2 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;

then consider W2 being Simplex of n,K such that

A48: w2 = W2 and

A49: U c= W2 ;

A50: ( SS1 is with_non-empty_elements & S = (center_of_mass V) .: SS1 ) by A27, A29, A32, RELAT_1:112;

w1 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;

then consider W1 being Simplex of n,K such that

A51: w1 = W1 and

A52: U c= W1 ;

A53: card W1 = (degree K) + 1 by A3, SIMPLEX0:def 18;

then A54: card W1 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A52, Th42;

then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;

then A55: ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;

A56: S \/ ((center_of_mass V) .: {W1}) <> S \/ ((center_of_mass V) .: {W2})

A63: X c= {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

then card W2 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W2) ) } = {(S \/ ((center_of_mass V) .: {W2}))} by A16, A30, A35, A36, A43, A49, Th42;

then S \/ ((center_of_mass V) .: {W2}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W2) ) } by TARSKI:def 1;

then ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W2}) & S c= R & conv (@ R) c= conv (@ W2) ) ;

then A77: S \/ ((center_of_mass V) .: {W2}) in X by A11;

S \/ ((center_of_mass V) .: {W1}) in X by A11, A55;

then {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} c= X by A77, ZFMISC_1:32;

then X = {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} by A63;

hence card X = 2 by A56, CARD_2:57; :: thesis: verum

end;then conv (@ U) meets Int A by A42, XBOOLE_1:63;

then A45: card { W where W is Simplex of n,K : U c= W } = 2 by A4, A44;

consider w1, w2 being object such that

A46: w1 <> w2 and

A47: { W where W is Simplex of n,K : U c= W } = {w1,w2} by A45, CARD_2:60;

w2 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;

then consider W2 being Simplex of n,K such that

A48: w2 = W2 and

A49: U c= W2 ;

A50: ( SS1 is with_non-empty_elements & S = (center_of_mass V) .: SS1 ) by A27, A29, A32, RELAT_1:112;

w1 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;

then consider W1 being Simplex of n,K such that

A51: w1 = W1 and

A52: U c= W1 ;

A53: card W1 = (degree K) + 1 by A3, SIMPLEX0:def 18;

then A54: card W1 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A52, Th42;

then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;

then A55: ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;

A56: S \/ ((center_of_mass V) .: {W1}) <> S \/ ((center_of_mass V) .: {W2})

proof

A62:
(card SS1) + Z <= degree K
by A3, A16, A27, A30, A33, Th33;
for A being Subset of K st A in {W1} holds

A is simplex-like by TARSKI:def 1;

then {W1} is simplex-like ;

then A57: SS1 \/ {W1} is simplex-like by TOPS_2:13;

A58: ( S \/ ((center_of_mass V) .: {W1}) = (center_of_mass V) .: (SS1 \/ {W1}) & S \/ ((center_of_mass V) .: {W2}) = (center_of_mass V) .: (SS1 \/ {W2}) ) by A35, RELAT_1:120;

W1 in {W1} by TARSKI:def 1;

then A59: W1 in SS1 \/ {W1} by XBOOLE_0:def 3;

for A being Subset of K st A in {W2} holds

A is simplex-like by TARSKI:def 1;

then {W2} is simplex-like ;

then A60: SS1 \/ {W2} is simplex-like by TOPS_2:13;

assume A61: S \/ ((center_of_mass V) .: {W1}) = S \/ ((center_of_mass V) .: {W2}) ; :: thesis: contradiction

not W1 is empty by A3, A53;

then SS1 \/ {W1} c= SS1 \/ {W2} by A12, A30, A55, A60, A58, A57, A61, Th34;

then ( W1 in SS1 or W1 in {W2} ) by A59, XBOOLE_0:def 3;

then W1 c= U by A46, A48, A51, TARSKI:def 1, ZFMISC_1:74;

then W1 = U by A52;

hence contradiction by A43, A54; :: thesis: verum

end;A is simplex-like by TARSKI:def 1;

then {W1} is simplex-like ;

then A57: SS1 \/ {W1} is simplex-like by TOPS_2:13;

A58: ( S \/ ((center_of_mass V) .: {W1}) = (center_of_mass V) .: (SS1 \/ {W1}) & S \/ ((center_of_mass V) .: {W2}) = (center_of_mass V) .: (SS1 \/ {W2}) ) by A35, RELAT_1:120;

W1 in {W1} by TARSKI:def 1;

then A59: W1 in SS1 \/ {W1} by XBOOLE_0:def 3;

for A being Subset of K st A in {W2} holds

A is simplex-like by TARSKI:def 1;

then {W2} is simplex-like ;

then A60: SS1 \/ {W2} is simplex-like by TOPS_2:13;

assume A61: S \/ ((center_of_mass V) .: {W1}) = S \/ ((center_of_mass V) .: {W2}) ; :: thesis: contradiction

not W1 is empty by A3, A53;

then SS1 \/ {W1} c= SS1 \/ {W2} by A12, A30, A55, A60, A58, A57, A61, Th34;

then ( W1 in SS1 or W1 in {W2} ) by A59, XBOOLE_0:def 3;

then W1 c= U by A46, A48, A51, TARSKI:def 1, ZFMISC_1:74;

then W1 = U by A52;

hence contradiction by A43, A54; :: thesis: verum

A63: X c= {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

proof

card W2 = (degree K) + 1
by A3, SIMPLEX0:def 18;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} )

A64: ( n + 1 = (degree K) + 1 & n = ((degree K) + 1) - 1 ) by A3, XXREAL_3:22, XXREAL_3:def 2;

assume x in X ; :: thesis: x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

then consider W being Simplex of n, BCS K such that

A65: x = W and

A66: S c= W by A11;

consider T being finite simplex-like Subset-Family of K such that

A67: T misses SS1 and

A68: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

A69: card T = Z + 1 and

A70: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A50, A62, A66, Th41;

consider t being object such that

A71: T = {t} by A69, CARD_2:42;

set TS = T \/ SS1;

A72: card (T \/ SS1) = n + 1 by A16, A36, A67, A69, CARD_2:40;

A73: union (T \/ SS1) in T \/ SS1 by A68, A71, SIMPLEX0:9;

T \/ SS1 is simplex-like by TOPS_2:13;

then reconsider UTS = union (T \/ SS1) as Simplex of K by A73;

Segm (card (T \/ SS1)) c= Segm (card UTS) by A68, SIMPLEX0:10;

then A74: card (T \/ SS1) <= card UTS by NAT_1:39;

UTS in T

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then card UTS <= n + 1 by A3, XXREAL_3:def 2;

then card UTS = n + 1 by A72, A74, XXREAL_0:1;

then A76: UTS is Simplex of n,K by A64, SIMPLEX0:48;

U c= UTS by XBOOLE_1:7, ZFMISC_1:77;

then UTS in { W where W is Simplex of n,K : U c= W } by A76;

then ( W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) or W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W2}) ) by A47, A48, A51, A70, A71, A75, TARSKI:def 2;

hence x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} by A35, A65, TARSKI:def 2; :: thesis: verum

end;A64: ( n + 1 = (degree K) + 1 & n = ((degree K) + 1) - 1 ) by A3, XXREAL_3:22, XXREAL_3:def 2;

assume x in X ; :: thesis: x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

then consider W being Simplex of n, BCS K such that

A65: x = W and

A66: S c= W by A11;

consider T being finite simplex-like Subset-Family of K such that

A67: T misses SS1 and

A68: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

A69: card T = Z + 1 and

A70: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A50, A62, A66, Th41;

consider t being object such that

A71: T = {t} by A69, CARD_2:42;

set TS = T \/ SS1;

A72: card (T \/ SS1) = n + 1 by A16, A36, A67, A69, CARD_2:40;

A73: union (T \/ SS1) in T \/ SS1 by A68, A71, SIMPLEX0:9;

T \/ SS1 is simplex-like by TOPS_2:13;

then reconsider UTS = union (T \/ SS1) as Simplex of K by A73;

Segm (card (T \/ SS1)) c= Segm (card UTS) by A68, SIMPLEX0:10;

then A74: card (T \/ SS1) <= card UTS by NAT_1:39;

UTS in T

proof

then A75:
UTS = t
by A71, TARSKI:def 1;
assume
not UTS in T
; :: thesis: contradiction

then UTS in SS1 by A73, XBOOLE_0:def 3;

then card UTS <= card U by NAT_1:43, ZFMISC_1:74;

hence contradiction by A43, A72, A74, NAT_1:13; :: thesis: verum

end;then UTS in SS1 by A73, XBOOLE_0:def 3;

then card UTS <= card U by NAT_1:43, ZFMISC_1:74;

hence contradiction by A43, A72, A74, NAT_1:13; :: thesis: verum

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then card UTS <= n + 1 by A3, XXREAL_3:def 2;

then card UTS = n + 1 by A72, A74, XXREAL_0:1;

then A76: UTS is Simplex of n,K by A64, SIMPLEX0:48;

U c= UTS by XBOOLE_1:7, ZFMISC_1:77;

then UTS in { W where W is Simplex of n,K : U c= W } by A76;

then ( W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) or W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W2}) ) by A47, A48, A51, A70, A71, A75, TARSKI:def 2;

hence x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} by A35, A65, TARSKI:def 2; :: thesis: verum

then card W2 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W2) ) } = {(S \/ ((center_of_mass V) .: {W2}))} by A16, A30, A35, A36, A43, A49, Th42;

then S \/ ((center_of_mass V) .: {W2}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W2) ) } by TARSKI:def 1;

then ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W2}) & S c= R & conv (@ R) c= conv (@ W2) ) ;

then A77: S \/ ((center_of_mass V) .: {W2}) in X by A11;

S \/ ((center_of_mass V) .: {W1}) in X by A11, A55;

then {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} c= X by A77, ZFMISC_1:32;

then X = {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} by A63;

hence card X = 2 by A56, CARD_2:57; :: thesis: verum

assume conv (@ S) misses Int A ; :: thesis: card X = 1

then consider BB being Subset of V such that

A79: BB c< A and

A80: conv (@ S) c= conv BB by A7, A78, RLAFFIN2:23;

A81: BB c= A by A79;

then reconsider B1 = BB as finite Subset of V ;

card B1 < n + 1 by A2, A79, CARD_2:48;

then A82: card B1 <= n by NAT_1:13;

Affin (@ S) c= Affin BB by A80, RLAFFIN1:68;

then n <= card B1 by A16, RLAFFIN1:79;

then card B1 = n by A82, XXREAL_0:1;

then card (A \ BB) = (n + 1) - n by A2, A81, CARD_2:44;

then consider ab being object such that

A83: A \ BB = {ab} by CARD_2:42;

not U is empty by A26, A43;

then @ U in dom (center_of_mass V) by A31, ZFMISC_1:56;

then A84: ( S c= conv (@ S) & (center_of_mass V) . U in @ S ) by A35, A38, FUNCT_1:def 6, RLAFFIN1:2;

then (center_of_mass V) . U in conv (@ S) ;

then A85: (center_of_mass V) . U in conv (@ U) by A42;

set BUU = ((center_of_mass V) . U) |-- (@ U);

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

then A86: @ U c= conv A by A41;

A87: ab in {ab} by TARSKI:def 1;

then reconsider ab = ab as Element of V by A83;

A88: ( SS1 is with_non-empty_elements & S = (center_of_mass V) .: SS1 ) by A27, A29, A32, RELAT_1:112;

A89: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;

then sum (((center_of_mass V) . U) |-- (@ U)) = 1 by A85, RLAFFIN1:def 7;

then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that

A90: ((Sum (((center_of_mass V) . U) |-- (@ U))) |-- A) . ab = Sum F and

A91: len G = len F and

G is one-to-one and

A92: rng G = Carrier (((center_of_mass V) . U) |-- (@ U)) and

A93: for n being Nat st n in dom F holds

F . n = ((((center_of_mass V) . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by A7, A86, RLAFFIN2:3;

A94: dom G = dom F by A91, FINSEQ_3:29;

U c= conv B1

proof

then
conv (@ U) c= conv B1
by CONVEX1:30;
A95:
Carrier (((center_of_mass V) . U) |-- (@ U)) c= U
by RLVECT_2:def 6;

then A101: (center_of_mass V) . U in conv BB by A80;

assume not U c= conv B1 ; :: thesis: contradiction

then consider t being object such that

A102: t in U and

A103: not t in conv B1 ;

reconsider tt = t as set by TARSKI:1;

A104: (t |-- A) . ab > 0

then t in Carrier (((center_of_mass V) . U) |-- (@ U)) by A102;

then consider n being object such that

A108: n in dom G and

A109: G . n = t by A92, FUNCT_1:def 3;

reconsider n = n as Nat by A108;

F . n = ((((center_of_mass V) . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by A93, A94, A108, A109;

then 0 < Sum F by A94, A96, A102, A104, A107, A108, RVSUM_1:85;

then A110: (((center_of_mass V) . U) |-- A) . ab > 0 by A85, A89, A90, RLAFFIN1:def 7;

Carrier (((center_of_mass V) . U) |-- BB) c= BB by RLVECT_2:def 6;

then A111: not ab in Carrier (((center_of_mass V) . U) |-- BB) by A83, A87, XBOOLE_0:def 5;

conv BB c= Affin BB by RLAFFIN1:65;

then ((center_of_mass V) . U) |-- A = ((center_of_mass V) . U) |-- BB by A7, A81, A101, RLAFFIN1:77;

hence contradiction by A111, A110; :: thesis: verum

end;A96: now :: thesis: for i being Nat st i in dom F holds

0 <= F . i

(center_of_mass V) . U in conv (@ S)
by A84;0 <= F . i

let i be Nat; :: thesis: ( i in dom F implies 0 <= F . i )

assume A97: i in dom F ; :: thesis: 0 <= F . i

A98: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A93, A97;

A99: G . i in rng G by A94, A97, FUNCT_1:def 3;

then G . i in U by A92, A95;

then A100: ((G . i) |-- A) . ab >= 0 by A7, A86, RLAFFIN1:71;

(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A92, A95, A99, RLAFFIN2:18;

hence 0 <= F . i by A98, A100; :: thesis: verum

end;assume A97: i in dom F ; :: thesis: 0 <= F . i

A98: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A93, A97;

A99: G . i in rng G by A94, A97, FUNCT_1:def 3;

then G . i in U by A92, A95;

then A100: ((G . i) |-- A) . ab >= 0 by A7, A86, RLAFFIN1:71;

(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A92, A95, A99, RLAFFIN2:18;

hence 0 <= F . i by A98, A100; :: thesis: verum

then A101: (center_of_mass V) . U in conv BB by A80;

assume not U c= conv B1 ; :: thesis: contradiction

then consider t being object such that

A102: t in U and

A103: not t in conv B1 ;

reconsider tt = t as set by TARSKI:1;

A104: (t |-- A) . ab > 0

proof

A107:
(((center_of_mass V) . U) |-- (@ U)) . t = 1 / (card U)
by A102, RLAFFIN2:18;
A \ {ab} c= B1

assume A106: (t |-- A) . ab <= 0 ; :: thesis: contradiction

(t |-- A) . ab >= 0 by A7, A86, A102, RLAFFIN1:71;

then for x being set st x in {ab} holds

(t |-- A) . x = 0 by A106, TARSKI:def 1;

then t in conv (A \ {ab}) by A7, A86, A102, RLAFFIN1:76;

hence contradiction by A103, A105; :: thesis: verum

end;proof

then A105:
conv (A \ {ab}) c= conv B1
by RLAFFIN1:3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ {ab} or x in B1 )

assume x in A \ {ab} ; :: thesis: x in B1

then ( x in A & not x in {ab} ) by XBOOLE_0:def 5;

hence x in B1 by A83, XBOOLE_0:def 5; :: thesis: verum

end;assume x in A \ {ab} ; :: thesis: x in B1

then ( x in A & not x in {ab} ) by XBOOLE_0:def 5;

hence x in B1 by A83, XBOOLE_0:def 5; :: thesis: verum

assume A106: (t |-- A) . ab <= 0 ; :: thesis: contradiction

(t |-- A) . ab >= 0 by A7, A86, A102, RLAFFIN1:71;

then for x being set st x in {ab} holds

(t |-- A) . x = 0 by A106, TARSKI:def 1;

then t in conv (A \ {ab}) by A7, A86, A102, RLAFFIN1:76;

hence contradiction by A103, A105; :: thesis: verum

then t in Carrier (((center_of_mass V) . U) |-- (@ U)) by A102;

then consider n being object such that

A108: n in dom G and

A109: G . n = t by A92, FUNCT_1:def 3;

reconsider n = n as Nat by A108;

F . n = ((((center_of_mass V) . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by A93, A94, A108, A109;

then 0 < Sum F by A94, A96, A102, A104, A107, A108, RVSUM_1:85;

then A110: (((center_of_mass V) . U) |-- A) . ab > 0 by A85, A89, A90, RLAFFIN1:def 7;

Carrier (((center_of_mass V) . U) |-- BB) c= BB by RLVECT_2:def 6;

then A111: not ab in Carrier (((center_of_mass V) . U) |-- BB) by A83, A87, XBOOLE_0:def 5;

conv BB c= Affin BB by RLAFFIN1:65;

then ((center_of_mass V) . U) |-- A = ((center_of_mass V) . U) |-- BB by A7, A81, A101, RLAFFIN1:77;

hence contradiction by A111, A110; :: thesis: verum

then conv (@ U) misses Int A by A79, RLAFFIN2:7, XBOOLE_1:63;

then card { W where W is Simplex of n,K : U c= W } = 1 by A4, A44;

then consider w1 being object such that

A112: { W where W is Simplex of n,K : U c= W } = {w1} by CARD_2:42;

w1 in { W where W is Simplex of n,K : U c= W } by A112, TARSKI:def 1;

then consider W1 being Simplex of n,K such that

A113: w1 = W1 and

A114: U c= W1 ;

A115: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;

A116: X c= {(S \/ ((center_of_mass V) .: {W1}))}

proof

card W1 = (degree K) + 1
by A3, SIMPLEX0:def 18;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {(S \/ ((center_of_mass V) .: {W1}))} )

A117: n + 1 = (degree K) + 1 by A3, XXREAL_3:def 2;

assume x in X ; :: thesis: x in {(S \/ ((center_of_mass V) .: {W1}))}

then consider W being Simplex of n, BCS K such that

A118: x = W and

A119: S c= W by A11;

consider T being finite simplex-like Subset-Family of K such that

A120: T misses SS1 and

A121: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

A122: card T = Z + 1 and

A123: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A88, A115, A119, Th41;

consider t being object such that

A124: T = {t} by A122, CARD_2:42;

set TS = T \/ SS1;

A125: card (T \/ SS1) = n + 1 by A16, A36, A120, A122, CARD_2:40;

A126: union (T \/ SS1) in T \/ SS1 by A121, A124, SIMPLEX0:9;

T \/ SS1 is simplex-like by TOPS_2:13;

then reconsider UTS = union (T \/ SS1) as Simplex of K by A126;

Segm (card (T \/ SS1)) c= Segm (card UTS) by A121, SIMPLEX0:10;

then A127: card (T \/ SS1) <= card UTS by NAT_1:39;

UTS in T

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then card UTS <= n + 1 by A3, XXREAL_3:def 2;

then ( card UTS = n + 1 & SS1 c= T \/ SS1 ) by A125, A127, XBOOLE_1:7, XXREAL_0:1;

then ( U c= UTS & UTS is Simplex of n,K ) by A3, A117, SIMPLEX0:def 18, ZFMISC_1:77;

then UTS in { W where W is Simplex of n,K : U c= W } ;

then W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) by A112, A113, A123, A124, A128, TARSKI:def 1;

hence x in {(S \/ ((center_of_mass V) .: {W1}))} by A35, A118, TARSKI:def 1; :: thesis: verum

end;A117: n + 1 = (degree K) + 1 by A3, XXREAL_3:def 2;

assume x in X ; :: thesis: x in {(S \/ ((center_of_mass V) .: {W1}))}

then consider W being Simplex of n, BCS K such that

A118: x = W and

A119: S c= W by A11;

consider T being finite simplex-like Subset-Family of K such that

A120: T misses SS1 and

A121: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

A122: card T = Z + 1 and

A123: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A88, A115, A119, Th41;

consider t being object such that

A124: T = {t} by A122, CARD_2:42;

set TS = T \/ SS1;

A125: card (T \/ SS1) = n + 1 by A16, A36, A120, A122, CARD_2:40;

A126: union (T \/ SS1) in T \/ SS1 by A121, A124, SIMPLEX0:9;

T \/ SS1 is simplex-like by TOPS_2:13;

then reconsider UTS = union (T \/ SS1) as Simplex of K by A126;

Segm (card (T \/ SS1)) c= Segm (card UTS) by A121, SIMPLEX0:10;

then A127: card (T \/ SS1) <= card UTS by NAT_1:39;

UTS in T

proof

then A128:
UTS = t
by A124, TARSKI:def 1;
assume
not UTS in T
; :: thesis: contradiction

then UTS in SS1 by A126, XBOOLE_0:def 3;

then card UTS <= card U by NAT_1:43, ZFMISC_1:74;

hence contradiction by A43, A125, A127, NAT_1:13; :: thesis: verum

end;then UTS in SS1 by A126, XBOOLE_0:def 3;

then card UTS <= card U by NAT_1:43, ZFMISC_1:74;

hence contradiction by A43, A125, A127, NAT_1:13; :: thesis: verum

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then card UTS <= n + 1 by A3, XXREAL_3:def 2;

then ( card UTS = n + 1 & SS1 c= T \/ SS1 ) by A125, A127, XBOOLE_1:7, XXREAL_0:1;

then ( U c= UTS & UTS is Simplex of n,K ) by A3, A117, SIMPLEX0:def 18, ZFMISC_1:77;

then UTS in { W where W is Simplex of n,K : U c= W } ;

then W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) by A112, A113, A123, A124, A128, TARSKI:def 1;

hence x in {(S \/ ((center_of_mass V) .: {W1}))} by A35, A118, TARSKI:def 1; :: thesis: verum

then card W1 = n + 1 by A3, XXREAL_3:def 2;

then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A114, Th42;

then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;

then ex R being Simplex of n, BCS K st

( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;

then S \/ ((center_of_mass V) .: {W1}) in X by A11;

then X = {(S \/ ((center_of_mass V) .: {W1}))} by A116, ZFMISC_1:33;

hence card X = 1 by CARD_1:30; :: thesis: verum

suppose A129:
card U = n + 1
; :: thesis: ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) )

A130:
conv (@ S) meets Int A

A166: card { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = 2 by A16, A30, A35, A36, A129, Th43;

consider w1, w2 being object such that

w1 <> w2 and

A167: { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = {w1,w2} by A166, CARD_2:60;

w2 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;

then consider W2 being Simplex of n, BCS K such that

A168: w2 = W2 and

A169: S c= W2 and

conv (@ W2) c= conv (@ U) ;

w1 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;

then consider W1 being Simplex of n, BCS K such that

A170: w1 = W1 and

A171: S c= W1 and

conv (@ W1) c= conv (@ U) ;

A172: W1 in X by A11, A171;

A173: X c= { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } c= X by A167, A170, A168, A172, ZFMISC_1:32;

hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A130, A166, A173, XBOOLE_0:def 10; :: thesis: verum

end;proof

set XX = { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } ;
not U is empty
by A129;

then @ U in dom (center_of_mass V) by A31, ZFMISC_1:56;

then A131: ( S c= conv (@ S) & (center_of_mass V) . U in @ S ) by A35, A38, FUNCT_1:def 6, RLAFFIN1:2;

then (center_of_mass V) . U in conv (@ S) ;

then A132: (center_of_mass V) . U in conv (@ U) by A42;

set BUU = ((center_of_mass V) . U) |-- (@ U);

assume A133: conv (@ S) misses Int A ; :: thesis: contradiction

( conv (@ S) c= conv A & not A is empty ) by A2, A41, A42;

then consider BB being Subset of V such that

A134: BB c< A and

A135: conv (@ S) c= conv BB by A7, A133, RLAFFIN2:23;

A136: BB c= A by A134;

then reconsider B1 = BB as finite Subset of V ;

Affin (@ S) c= Affin BB by A135, RLAFFIN1:68;

then A137: n <= card B1 by A16, RLAFFIN1:79;

A138: card B1 < n + 1 by A2, A134, CARD_2:48;

then card B1 <= n by NAT_1:13;

then card B1 = n by A137, XXREAL_0:1;

then card (A \ BB) = (n + 1) - n by A2, A136, CARD_2:44;

then consider ab being object such that

A139: A \ BB = {ab} by CARD_2:42;

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

then A140: @ U c= conv A by A41;

A141: ab in {ab} by TARSKI:def 1;

then reconsider ab = ab as Element of V by A139;

A142: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;

then sum (((center_of_mass V) . U) |-- (@ U)) = 1 by A132, RLAFFIN1:def 7;

then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that

A143: ((Sum (((center_of_mass V) . U) |-- (@ U))) |-- A) . ab = Sum F and

A144: len G = len F and

G is one-to-one and

A145: rng G = Carrier (((center_of_mass V) . U) |-- (@ U)) and

A146: for n being Nat st n in dom F holds

F . n = ((((center_of_mass V) . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by A7, A140, RLAFFIN2:3;

A147: dom G = dom F by A144, FINSEQ_3:29;

A148: A \ {ab} = A /\ BB by A139, XBOOLE_1:48

.= BB by A136, XBOOLE_1:28 ;

U c= conv B1

then Affin (@ U) c= Affin B1 by RLAFFIN1:68;

hence contradiction by A129, A138, RLAFFIN1:79; :: thesis: verum

end;then @ U in dom (center_of_mass V) by A31, ZFMISC_1:56;

then A131: ( S c= conv (@ S) & (center_of_mass V) . U in @ S ) by A35, A38, FUNCT_1:def 6, RLAFFIN1:2;

then (center_of_mass V) . U in conv (@ S) ;

then A132: (center_of_mass V) . U in conv (@ U) by A42;

set BUU = ((center_of_mass V) . U) |-- (@ U);

assume A133: conv (@ S) misses Int A ; :: thesis: contradiction

( conv (@ S) c= conv A & not A is empty ) by A2, A41, A42;

then consider BB being Subset of V such that

A134: BB c< A and

A135: conv (@ S) c= conv BB by A7, A133, RLAFFIN2:23;

A136: BB c= A by A134;

then reconsider B1 = BB as finite Subset of V ;

Affin (@ S) c= Affin BB by A135, RLAFFIN1:68;

then A137: n <= card B1 by A16, RLAFFIN1:79;

A138: card B1 < n + 1 by A2, A134, CARD_2:48;

then card B1 <= n by NAT_1:13;

then card B1 = n by A137, XXREAL_0:1;

then card (A \ BB) = (n + 1) - n by A2, A136, CARD_2:44;

then consider ab being object such that

A139: A \ BB = {ab} by CARD_2:42;

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

then A140: @ U c= conv A by A41;

A141: ab in {ab} by TARSKI:def 1;

then reconsider ab = ab as Element of V by A139;

A142: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;

then sum (((center_of_mass V) . U) |-- (@ U)) = 1 by A132, RLAFFIN1:def 7;

then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that

A143: ((Sum (((center_of_mass V) . U) |-- (@ U))) |-- A) . ab = Sum F and

A144: len G = len F and

G is one-to-one and

A145: rng G = Carrier (((center_of_mass V) . U) |-- (@ U)) and

A146: for n being Nat st n in dom F holds

F . n = ((((center_of_mass V) . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by A7, A140, RLAFFIN2:3;

A147: dom G = dom F by A144, FINSEQ_3:29;

A148: A \ {ab} = A /\ BB by A139, XBOOLE_1:48

.= BB by A136, XBOOLE_1:28 ;

U c= conv B1

proof

then
conv (@ U) c= conv B1
by CONVEX1:30;
A149:
Carrier (((center_of_mass V) . U) |-- (@ U)) c= U
by RLVECT_2:def 6;

then A155: (center_of_mass V) . U in conv BB by A135;

assume not U c= conv B1 ; :: thesis: contradiction

then consider t being object such that

A156: t in U and

A157: not t in conv B1 ;

reconsider tt = t as set by TARSKI:1;

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

then A158: t in conv (@ U) by A156;

A159: (t |-- A) . ab > 0

then t in Carrier (((center_of_mass V) . U) |-- (@ U)) by A156;

then consider n being object such that

A162: n in dom G and

A163: G . n = t by A145, FUNCT_1:def 3;

reconsider n = n as Nat by A162;

F . n = ((((center_of_mass V) . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by A146, A147, A162, A163;

then 0 < Sum F by A147, A150, A156, A159, A161, A162, RVSUM_1:85;

then A164: (((center_of_mass V) . U) |-- A) . ab > 0 by A132, A142, A143, RLAFFIN1:def 7;

Carrier (((center_of_mass V) . U) |-- BB) c= BB by RLVECT_2:def 6;

then A165: not ab in Carrier (((center_of_mass V) . U) |-- BB) by A139, A141, XBOOLE_0:def 5;

conv BB c= Affin BB by RLAFFIN1:65;

then ((center_of_mass V) . U) |-- A = ((center_of_mass V) . U) |-- BB by A7, A136, A155, RLAFFIN1:77;

hence contradiction by A165, A164; :: thesis: verum

end;A150: now :: thesis: for i being Nat st i in dom F holds

0 <= F . i

(center_of_mass V) . U in conv (@ S)
by A131;0 <= F . i

let i be Nat; :: thesis: ( i in dom F implies 0 <= F . i )

assume A151: i in dom F ; :: thesis: 0 <= F . i

A152: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A146, A151;

A153: G . i in rng G by A147, A151, FUNCT_1:def 3;

then G . i in U by A145, A149;

then A154: ((G . i) |-- A) . ab >= 0 by A7, A140, RLAFFIN1:71;

(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A145, A149, A153, RLAFFIN2:18;

hence 0 <= F . i by A152, A154; :: thesis: verum

end;assume A151: i in dom F ; :: thesis: 0 <= F . i

A152: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A146, A151;

A153: G . i in rng G by A147, A151, FUNCT_1:def 3;

then G . i in U by A145, A149;

then A154: ((G . i) |-- A) . ab >= 0 by A7, A140, RLAFFIN1:71;

(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A145, A149, A153, RLAFFIN2:18;

hence 0 <= F . i by A152, A154; :: thesis: verum

then A155: (center_of_mass V) . U in conv BB by A135;

assume not U c= conv B1 ; :: thesis: contradiction

then consider t being object such that

A156: t in U and

A157: not t in conv B1 ;

reconsider tt = t as set by TARSKI:1;

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

then A158: t in conv (@ U) by A156;

A159: (t |-- A) . ab > 0

proof

A161:
(((center_of_mass V) . U) |-- (@ U)) . t = 1 / (card U)
by A156, RLAFFIN2:18;
assume A160:
(t |-- A) . ab <= 0
; :: thesis: contradiction

(t |-- A) . ab >= 0 by A7, A41, A158, RLAFFIN1:71;

then for y being set st y in A \ B1 holds

(t |-- A) . y = 0 by A139, A160, TARSKI:def 1;

hence contradiction by A7, A41, A139, A148, A157, A158, RLAFFIN1:76; :: thesis: verum

end;(t |-- A) . ab >= 0 by A7, A41, A158, RLAFFIN1:71;

then for y being set st y in A \ B1 holds

(t |-- A) . y = 0 by A139, A160, TARSKI:def 1;

hence contradiction by A7, A41, A139, A148, A157, A158, RLAFFIN1:76; :: thesis: verum

then t in Carrier (((center_of_mass V) . U) |-- (@ U)) by A156;

then consider n being object such that

A162: n in dom G and

A163: G . n = t by A145, FUNCT_1:def 3;

reconsider n = n as Nat by A162;

F . n = ((((center_of_mass V) . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by A146, A147, A162, A163;

then 0 < Sum F by A147, A150, A156, A159, A161, A162, RVSUM_1:85;

then A164: (((center_of_mass V) . U) |-- A) . ab > 0 by A132, A142, A143, RLAFFIN1:def 7;

Carrier (((center_of_mass V) . U) |-- BB) c= BB by RLVECT_2:def 6;

then A165: not ab in Carrier (((center_of_mass V) . U) |-- BB) by A139, A141, XBOOLE_0:def 5;

conv BB c= Affin BB by RLAFFIN1:65;

then ((center_of_mass V) . U) |-- A = ((center_of_mass V) . U) |-- BB by A7, A136, A155, RLAFFIN1:77;

hence contradiction by A165, A164; :: thesis: verum

then Affin (@ U) c= Affin B1 by RLAFFIN1:68;

hence contradiction by A129, A138, RLAFFIN1:79; :: thesis: verum

A166: card { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = 2 by A16, A30, A35, A36, A129, Th43;

consider w1, w2 being object such that

w1 <> w2 and

A167: { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = {w1,w2} by A166, CARD_2:60;

w2 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;

then consider W2 being Simplex of n, BCS K such that

A168: w2 = W2 and

A169: S c= W2 and

conv (@ W2) c= conv (@ U) ;

w1 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;

then consider W1 being Simplex of n, BCS K such that

A170: w1 = W1 and

A171: S c= W1 and

conv (@ W1) c= conv (@ U) ;

A172: W1 in X by A11, A171;

A173: X c= { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

proof

W2 in X
by A11, A169;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in X or w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } )

assume w in X ; :: thesis: w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

then consider W being Simplex of n, BCS K such that

A174: w = W and

A175: S c= W by A11;

(card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;

then consider T being finite simplex-like Subset-Family of K such that

T misses SS1 and

A176: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

card T = Z + 1 and

A177: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A27, A30, A33, A34, A175, Th41;

reconsider TS = T \/ SS1 as finite simplex-like Subset-Family of K by TOPS_2:13;

A178: W = (center_of_mass V) .: (@ TS) by A177, RELAT_1:120;

union TS in TS by A37, A176, SIMPLEX0:9;

then reconsider UTS = union TS as Simplex of K by TOPS_2:def 1;

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then A179: card UTS <= n + 1 by A3, XXREAL_3:def 2;

A180: U c= union TS by XBOOLE_1:7, ZFMISC_1:77;

then n + 1 <= card UTS by A129, NAT_1:43;

then UTS = U by A129, A179, A180, CARD_2:102, XXREAL_0:1;

then conv (@ W) c= conv (@ U) by A178, CONVEX1:30, RLAFFIN2:17;

hence w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A174, A175; :: thesis: verum

end;assume w in X ; :: thesis: w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

then consider W being Simplex of n, BCS K such that

A174: w = W and

A175: S c= W by A11;

(card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;

then consider T being finite simplex-like Subset-Family of K such that

T misses SS1 and

A176: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and

card T = Z + 1 and

A177: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A27, A30, A33, A34, A175, Th41;

reconsider TS = T \/ SS1 as finite simplex-like Subset-Family of K by TOPS_2:13;

A178: W = (center_of_mass V) .: (@ TS) by A177, RELAT_1:120;

union TS in TS by A37, A176, SIMPLEX0:9;

then reconsider UTS = union TS as Simplex of K by TOPS_2:def 1;

card UTS <= (degree K) + 1 by SIMPLEX0:24;

then A179: card UTS <= n + 1 by A3, XXREAL_3:def 2;

A180: U c= union TS by XBOOLE_1:7, ZFMISC_1:77;

then n + 1 <= card UTS by A129, NAT_1:43;

then UTS = U by A129, A179, A180, CARD_2:102, XXREAL_0:1;

then conv (@ W) c= conv (@ U) by A178, CONVEX1:30, RLAFFIN2:17;

hence w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A174, A175; :: thesis: verum

then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } c= X by A167, A170, A168, A172, ZFMISC_1:32;

hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A130, A166, A173, XBOOLE_0:def 10; :: thesis: verum