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

|.().| = conv A by Th8;
then A5: |.K.| = conv A by ;
A6: K is finite-degree by ;
A7: A is affinely-independent
proof
consider a being Subset of K such that
A8: a is simplex-like and
A9: card a = () + 1 by ;
conv (@ a) c= conv A by A5, A8, Th5;
then A10: Affin (@ a) c= Affin A by RLAFFIN1:68;
card A = card a by ;
hence A is affinely-independent by ; :: thesis: verum
end;
set B = center_of_mass V;
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 ;
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 ((),K) by ;
per cases ( n = 0 or n > 0 ) ;
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 ;
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 ;
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
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 ;
then reconsider w = W as Simplex of (BCS K) by PRE_TOPC:def 2;
card W = () + 1 by ;
then w is Simplex of n, BCS K by ;
hence x in X by ; :: thesis: verum
end;
A24: X c= { W where W is Simplex of n,K : s c= W }
proof
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 ;
then reconsider w = W as Simplex of K by PRE_TOPC:def 2;
card W = (degree (BCS K)) + 1 by ;
then w is Simplex of n,K by ;
hence x in { W where W is Simplex of n,K : s c= W } by A25; :: thesis: verum
end;
( conv (@ S) misses Int A implies card { W where W is Simplex of n,K : s c= W } = 1 ) by ;
hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by ; :: thesis: verum
end;
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 = () .: SS by ;
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 ;
A29: not {} in SS1 by ZFMISC_1:56;
then A30: SS1 is with_non-empty_elements ;
A31: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
then A32: SS /\ () = (SS /\ (bool the carrier of V)) \ by XBOOLE_1:49
.= SS1 /\ (bool the carrier of V) by XBOOLE_1:49
.= SS1 by ;
then A33: (center_of_mass V) .: SS = () .: SS1 by RELAT_1:112;
then A34: card SS1 = n by ;
A35: S = () .: SS1 by ;
A36: card SS1 = card S by ;
then A37: not SS1 is empty by ;
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 ;
then A39: n <= card U by ;
card U <= () + 1 by SIMPLEX0:24;
then A40: card U <= n + 1 by ;
A41: conv (@ U) c= conv A by ;
SS1 c= bool the carrier of V by A28;
then A42: conv (@ S) c= conv (@ U) by ;
per cases ( card U = n or card U = n + 1 ) by ;
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 ;
hereby :: thesis: ( conv (@ S) misses Int A implies card X = 1 )
assume conv (@ S) meets Int A ; :: thesis: card X = 2
then conv (@ U) meets Int A by ;
then A45: card { W where W is Simplex of n,K : U c= W } = 2 by ;
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 ;
w2 in { W where W is Simplex of n,K : U c= W } by ;
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 = () .: SS1 ) by ;
w1 in { W where W is Simplex of n,K : U c= W } by ;
then consider W1 being Simplex of n,K such that
A51: w1 = W1 and
A52: U c= W1 ;
A53: card W1 = () + 1 by ;
then A54: card W1 = n + 1 by ;
then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ (() .: {W1}))} by A16, A27, A30, A33, A36, A43, A52, Th42;
then S \/ (() .: {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 \/ (() .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;
A56: S \/ (() .: {W1}) <> S \/ (() .: {W2})
proof
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 \/ (() .: {W1}) = () .: (SS1 \/ {W1}) & S \/ (() .: {W2}) = () .: (SS1 \/ {W2}) ) by ;
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 \/ (() .: {W1}) = S \/ (() .: {W2}) ; :: thesis: contradiction
not W1 is empty by ;
then SS1 \/ {W1} c= SS1 \/ {W2} by A12, A30, A55, A60, A58, A57, A61, Th34;
then ( W1 in SS1 or W1 in {W2} ) by ;
then W1 c= U by ;
then W1 = U by A52;
hence contradiction by A43, A54; :: thesis: verum
end;
A62: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;
A63: X c= {(S \/ (() .: {W1})),(S \/ (() .: {W2}))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {(S \/ (() .: {W1})),(S \/ (() .: {W2}))} )
A64: ( n + 1 = () + 1 & n = (() + 1) - 1 ) by ;
assume x in X ; :: thesis: x in {(S \/ (() .: {W1})),(S \/ (() .: {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 = (() .: SS1) \/ (() .: T) by A16, A36, A50, A62, A66, Th41;
consider t being object such that
A71: T = {t} by ;
set TS = T \/ SS1;
A72: card (T \/ SS1) = n + 1 by ;
A73: union (T \/ SS1) in T \/ SS1 by ;
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 ;
then A74: card (T \/ SS1) <= card UTS by NAT_1:39;
UTS in T
proof
assume not UTS in T ; :: thesis: contradiction
then UTS in SS1 by ;
then card UTS <= card U by ;
hence contradiction by A43, A72, A74, NAT_1:13; :: thesis: verum
end;
then A75: UTS = t by ;
card UTS <= () + 1 by SIMPLEX0:24;
then card UTS <= n + 1 by ;
then card UTS = n + 1 by ;
then A76: UTS is Simplex of n,K by ;
U c= UTS by ;
then UTS in { W where W is Simplex of n,K : U c= W } by A76;
then ( W = (() .: SS1) \/ (() .: {W1}) or W = (() .: SS1) \/ (() .: {W2}) ) by ;
hence x in {(S \/ (() .: {W1})),(S \/ (() .: {W2}))} by ; :: thesis: verum
end;
card W2 = () + 1 by ;
then card W2 = n + 1 by ;
then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W2) ) } = {(S \/ (() .: {W2}))} by A16, A30, A35, A36, A43, A49, Th42;
then S \/ (() .: {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 \/ (() .: {W2}) & S c= R & conv (@ R) c= conv (@ W2) ) ;
then A77: S \/ (() .: {W2}) in X by A11;
S \/ (() .: {W1}) in X by ;
then {(S \/ (() .: {W1})),(S \/ (() .: {W2}))} c= X by ;
then X = {(S \/ (() .: {W1})),(S \/ (() .: {W2}))} by A63;
hence card X = 2 by ; :: thesis: verum
end;
A78: ( conv (@ S) c= conv A & not A is empty ) by A2, A41, A42;
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 ;
A81: BB c= A by A79;
then reconsider B1 = BB as finite Subset of V ;
card B1 < n + 1 by ;
then A82: card B1 <= n by NAT_1:13;
Affin (@ S) c= Affin BB by ;
then n <= card B1 by ;
then card B1 = n by ;
then card (A \ BB) = (n + 1) - n by ;
then consider ab being object such that
A83: A \ BB = {ab} by CARD_2:42;
not U is empty by ;
then @ U in dom () by ;
then A84: ( S c= conv (@ S) & () . U in @ S ) by ;
then (center_of_mass V) . U in conv (@ S) ;
then A85: (center_of_mass V) . U in conv (@ U) by A42;
set BUU = (() . 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 = () .: SS1 ) by ;
A89: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;
then sum ((() . U) |-- (@ U)) = 1 by ;
then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that
A90: ((Sum ((() . U) |-- (@ U))) |-- A) . ab = Sum F and
A91: len G = len F and
G is one-to-one and
A92: rng G = Carrier ((() . U) |-- (@ U)) and
A93: for n being Nat st n in dom F holds
F . n = (((() . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by ;
A94: dom G = dom F by ;
U c= conv B1
proof
A95: Carrier ((() . U) |-- (@ U)) c= U by RLVECT_2:def 6;
A96: now :: thesis: for i being Nat st i in dom F holds
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 = (((() . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by ;
A99: G . i in rng G by ;
then G . i in U by ;
then A100: ((G . i) |-- A) . ab >= 0 by ;
(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by ;
hence 0 <= F . i by ; :: thesis: verum
end;
(center_of_mass V) . U in conv (@ S) by A84;
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
A \ {ab} c= B1
proof
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 ; :: thesis: verum
end;
then A105: conv (A \ {ab}) c= conv B1 by RLAFFIN1:3;
assume A106: (t |-- A) . ab <= 0 ; :: thesis: contradiction
(t |-- A) . ab >= 0 by ;
then for x being set st x in {ab} holds
(t |-- A) . x = 0 by ;
then t in conv (A \ {ab}) by ;
hence contradiction by A103, A105; :: thesis: verum
end;
A107: (((center_of_mass V) . U) |-- (@ U)) . t = 1 / (card U) by ;
then t in Carrier ((() . U) |-- (@ U)) by A102;
then consider n being object such that
A108: n in dom G and
A109: G . n = t by ;
reconsider n = n as Nat by A108;
F . n = (((() . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by ;
then 0 < Sum F by ;
then A110: (((center_of_mass V) . U) |-- A) . ab > 0 by ;
Carrier ((() . U) |-- BB) c= BB by RLVECT_2:def 6;
then A111: not ab in Carrier ((() . U) |-- BB) by ;
conv BB c= Affin BB by RLAFFIN1:65;
then ((center_of_mass V) . U) |-- A = (() . U) |-- BB by ;
hence contradiction by A111, A110; :: thesis: verum
end;
then conv (@ U) c= conv B1 by CONVEX1:30;
then conv (@ U) misses Int A by ;
then card { W where W is Simplex of n,K : U c= W } = 1 by ;
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 ;
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 \/ (() .: {W1}))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {(S \/ (() .: {W1}))} )
A117: n + 1 = () + 1 by ;
assume x in X ; :: thesis: x in {(S \/ (() .: {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 = (() .: SS1) \/ (() .: T) by ;
consider t being object such that
A124: T = {t} by ;
set TS = T \/ SS1;
A125: card (T \/ SS1) = n + 1 by ;
A126: union (T \/ SS1) in T \/ SS1 by ;
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 ;
then A127: card (T \/ SS1) <= card UTS by NAT_1:39;
UTS in T
proof
assume not UTS in T ; :: thesis: contradiction
then UTS in SS1 by ;
then card UTS <= card U by ;
hence contradiction by A43, A125, A127, NAT_1:13; :: thesis: verum
end;
then A128: UTS = t by ;
card UTS <= () + 1 by SIMPLEX0:24;
then card UTS <= n + 1 by ;
then ( card UTS = n + 1 & SS1 c= T \/ SS1 ) by ;
then ( U c= UTS & UTS is Simplex of n,K ) by ;
then UTS in { W where W is Simplex of n,K : U c= W } ;
then W = (() .: SS1) \/ (() .: {W1}) by ;
hence x in {(S \/ (() .: {W1}))} by ; :: thesis: verum
end;
card W1 = () + 1 by ;
then card W1 = n + 1 by ;
then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ (() .: {W1}))} by A16, A27, A30, A33, A36, A43, A114, Th42;
then S \/ (() .: {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 \/ (() .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;
then S \/ (() .: {W1}) in X by A11;
then X = {(S \/ (() .: {W1}))} by ;
hence card X = 1 by CARD_1:30; :: thesis: verum
end;
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
proof
not U is empty by A129;
then @ U in dom () by ;
then A131: ( S c= conv (@ S) & () . U in @ S ) by ;
then (center_of_mass V) . U in conv (@ S) ;
then A132: (center_of_mass V) . U in conv (@ U) by A42;
set BUU = (() . 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 ;
A136: BB c= A by A134;
then reconsider B1 = BB as finite Subset of V ;
Affin (@ S) c= Affin BB by ;
then A137: n <= card B1 by ;
A138: card B1 < n + 1 by ;
then card B1 <= n by NAT_1:13;
then card B1 = n by ;
then card (A \ BB) = (n + 1) - n by ;
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 ((() . U) |-- (@ U)) = 1 by ;
then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that
A143: ((Sum ((() . U) |-- (@ U))) |-- A) . ab = Sum F and
A144: len G = len F and
G is one-to-one and
A145: rng G = Carrier ((() . U) |-- (@ U)) and
A146: for n being Nat st n in dom F holds
F . n = (((() . U) |-- (@ U)) . (G . n)) * (((G . n) |-- A) . ab) by ;
A147: dom G = dom F by ;
A148: A \ {ab} = A /\ BB by
.= BB by ;
U c= conv B1
proof
A149: Carrier ((() . U) |-- (@ U)) c= U by RLVECT_2:def 6;
A150: now :: thesis: for i being Nat st i in dom F holds
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 = (((() . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by ;
A153: G . i in rng G by ;
then G . i in U by ;
then A154: ((G . i) |-- A) . ab >= 0 by ;
(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by ;
hence 0 <= F . i by ; :: thesis: verum
end;
(center_of_mass V) . U in conv (@ S) by A131;
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
assume A160: (t |-- A) . ab <= 0 ; :: thesis: contradiction
(t |-- A) . ab >= 0 by ;
then for y being set st y in A \ B1 holds
(t |-- A) . y = 0 by ;
hence contradiction by A7, A41, A139, A148, A157, A158, RLAFFIN1:76; :: thesis: verum
end;
A161: (((center_of_mass V) . U) |-- (@ U)) . t = 1 / (card U) by ;
then t in Carrier ((() . U) |-- (@ U)) by A156;
then consider n being object such that
A162: n in dom G and
A163: G . n = t by ;
reconsider n = n as Nat by A162;
F . n = (((() . U) |-- (@ U)) . tt) * ((t |-- A) . ab) by ;
then 0 < Sum F by ;
then A164: (((center_of_mass V) . U) |-- A) . ab > 0 by ;
Carrier ((() . U) |-- BB) c= BB by RLVECT_2:def 6;
then A165: not ab in Carrier ((() . U) |-- BB) by ;
conv BB c= Affin BB by RLAFFIN1:65;
then ((center_of_mass V) . U) |-- A = (() . U) |-- BB by ;
hence contradiction by A165, A164; :: thesis: verum
end;
then conv (@ U) c= conv B1 by CONVEX1:30;
then Affin (@ U) c= Affin B1 by RLAFFIN1:68;
hence contradiction by A129, A138, RLAFFIN1:79; :: thesis: verum
end;
set XX = { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } ;
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 ;
w2 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by ;
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 ;
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 ;
A173: X c= { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }
proof
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 = (() .: SS1) \/ (() .: 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 = () .: (@ TS) by ;
union TS in TS by ;
then reconsider UTS = union TS as Simplex of K by TOPS_2:def 1;
card UTS <= () + 1 by SIMPLEX0:24;
then A179: card UTS <= n + 1 by ;
A180: U c= union TS by ;
then n + 1 <= card UTS by ;
then UTS = U by ;
then conv (@ W) c= conv (@ U) by ;
hence w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by ; :: thesis: verum
end;
W2 in X by ;
then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } c= X by ;
hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by ; :: thesis: verum
end;
end;
end;
end;