let n be Nat; :: thesis:
let V be RealLinearSpace; :: thesis:
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis:
reconsider Z = 0 as Nat ;
let A be finite Subset of V; :: thesis:
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:
|.(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

reconsider d = degree K as ext-real number ;
consider a being Subset of K such that
A8: not a is dependent 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:

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 ext-real number ;
let S be Simplex of n - 1, BCS K; :: thesis:
let X be set ; :: thesis:
assume A11: X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } ; :: thesis:
[#] 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:33, XREAL_1:148;
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 ;

suppose A18: n = 0 ; :: thesis:

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 5;
then reconsider s = S as Simplex of K by PRE_TOPC:def 5;
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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { W where W is Simplex of n,K : s c= W } ; :: thesis:
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 5;
then reconsider w = W as Simplex of (BCS K) by PRE_TOPC:def 5;
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:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
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 5;
then reconsider w = W as Simplex of K by PRE_TOPC:def 5;
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:

end;

( conv (@ S) misses Int A implies card { W where W is Simplex of n,K : s c= W } = 1 ) by A4, A20;
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:

end;

suppose A26: n > 0 ; :: thesis:

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:18;
A28: ( SS1 c= bool (@ (union SS1)) & bool (@ (union SS1)) c= bool the carrier of V ) by ZFMISC_1:79, ZFMISC_1:100;
A29: not {} in SS1 by ZFMISC_1:64;
then A30: SS1 is with_non-empty_elements by SETFAM_1:def 9;
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:145;
then A34: card SS1 = n by A16, A27, A30, Th33;
A35: S = (center_of_mass V) .: SS1 by A27, A32, RELAT_1:145;
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;
card SS1 c= card U by A30, SIMPLEX0:10;
then A39: n <= card U by A16, A36, NAT_1:40;
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, XBOOLE_1:1;
then A42: conv (@ S) c= conv (@ U) by A35, CONVEX1:30, RLAFFIN2:17;

per cases by A39, A40, NAT_1:9;

suppose A43: card U = n ; :: thesis:

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;

hereby :: thesis:

assume conv (@ S) meets Int A ; :: thesis:
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;
then { W where W is Simplex of n,K : U c= W } is finite ;
then consider w1, w2 being set such that
A46: w1 <> w2 and
A47: { W where W is Simplex of n,K : U c= W } = {w1,w2} by A45, CARD_2:79;
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:145, SETFAM_1:def 9;
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

for A being Subset of K st A in {W1} holds
not A is dependent by TARSKI:def 1;
then {W1} is simplex-like by TOPS_2:def 1;
then A57: SS1 \/ {W1} is simplex-like by TOPS_2:20;
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:153;
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
not A is dependent by TARSKI:def 1;
then {W2} is simplex-like by TOPS_2:def 1;
then A60: SS1 \/ {W2} is simplex-like by TOPS_2:20;
assume A61: S \/ ((center_of_mass V) .: {W1}) = S \/ ((center_of_mass V) .: {W2}) ; :: thesis:
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:92;
then W1 = U by A52, XBOOLE_0:def 10;
hence contradiction by A43, A54; :: thesis:

end;

A62: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;
A63: X c= {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
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 set such that
A71: T = {t} by A69, CARD_2:60;
set TS = T \/ SS1;
A72: card (T \/ SS1) = n + 1 by A16, A36, A67, A69, CARD_2:53;
A73: union (T \/ SS1) in T \/ SS1 by A68, A71, SIMPLEX0:9;
T \/ SS1 is simplex-like by TOPS_2:20;
then reconsider UTS = union (T \/ SS1) as Simplex of K by A73, TOPS_2:def 1;
card (T \/ SS1) c= card UTS by A68, SIMPLEX0:10;
then A74: card (T \/ SS1) <= card UTS by NAT_1:40;
UTS in T

proof

assume not UTS in T ; :: thesis:
then UTS in SS1 by A73, XBOOLE_0:def 3;
then card UTS <= card U by NAT_1:44, ZFMISC_1:92;
hence contradiction by A43, A72, A74, NAT_1:13; :: thesis:

end;

then A75: UTS = t by A71, TARSKI:def 1;
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:95;
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:

end;

end;

proof

A95: Carrier (((center_of_mass V) . U) |-- (@ U)) c= U by RLVECT_2:def 8;

A96: now

let i be Nat; :: thesis:
assume A97: i in dom F ; :: thesis:
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 5;
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:

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:
then consider t being set such that
A102: t in U and
A103: not t in conv B1 by TARSKI:def 3;
A104: (t |-- A) . ab > 0

proof

A \ {ab} c= B1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in A \ {ab} ; :: thesis:
then ( x in A & not x in {ab} ) by XBOOLE_0:def 5;
hence x in B1 by A83, XBOOLE_0:def 5; :: thesis:

end;

then A105: conv (A \ {ab}) c= conv B1 by RLAFFIN1:3;
assume A106: (t |-- A) . ab <= 0 ; :: thesis:
(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:

end;

end;

then conv (@ U) c= conv B1 by CONVEX1:30;
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 set such that
A112: { W where W is Simplex of n,K : U c= W } = {w1} by CARD_2:60;
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

let x be set ; :: according to TARSKI:def 3 :: thesis:
A117: n + 1 = (degree K) + 1 by A3, XXREAL_3:def 2;
assume x in X ; :: thesis:
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 set such that
A124: T = {t} by A122, CARD_2:60;
set TS = T \/ SS1;
A125: card (T \/ SS1) = n + 1 by A16, A36, A120, A122, CARD_2:53;
A126: union (T \/ SS1) in T \/ SS1 by A121, A124, SIMPLEX0:9;
T \/ SS1 is simplex-like by TOPS_2:20;
then reconsider UTS = union (T \/ SS1) as Simplex of K by A126, TOPS_2:def 1;
card (T \/ SS1) c= card UTS by A121, SIMPLEX0:10;
then A127: card (T \/ SS1) <= card UTS by NAT_1:40;
UTS in T

proof

assume not UTS in T ; :: thesis:
then UTS in SS1 by A126, XBOOLE_0:def 3;
then card UTS <= card U by NAT_1:44, ZFMISC_1:92;
hence contradiction by A43, A125, A127, NAT_1:13; :: thesis:

end;

then A128: UTS = t by A124, TARSKI:def 1;
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, XXREAL_0:1, XBOOLE_1:7;
then ( U c= UTS & UTS is Simplex of n,K ) by A3, A117, SIMPLEX0:def 18, ZFMISC_1:95;
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:

end;

card W1 = (degree K) + 1 by A3, SIMPLEX0:def 18;
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:39;
hence card X = 1 by CARD_1:50; :: thesis:
set BUA = ((center_of_mass V) . U) |-- A;

end;

suppose A130: card U = n + 1 ; :: thesis:

A131: conv (@ S) meets Int A

proof

not U is empty by A130;
then @ U in dom (center_of_mass V) by A31, ZFMISC_1:64;
then A132: ( S c= conv (@ S) & (center_of_mass V) . U in @ S ) by A35, A38, FUNCT_1:def 12, RLAFFIN1:2;
then (center_of_mass V) . U in conv (@ S) ;
then A133: (center_of_mass V) . U in conv (@ U) by A42;
set BUA = ((center_of_mass V) . U) |-- A;
set BUU = ((center_of_mass V) . U) |-- (@ U);
assume A134: conv (@ S) misses Int A ; :: thesis:
( conv (@ S) c= conv A & not A is empty ) by A2, A41, A42, XBOOLE_1:1;
then consider BB being Subset of V such that
A135: BB c< A and
A136: conv (@ S) c= conv BB by A7, A134, RLAFFIN2:23;
A137: BB c= A by A135, XBOOLE_0:def 8;
then reconsider B1 = BB as finite Subset of V ;
Affin (@ S) c= Affin BB by A136, RLAFFIN1:68;
then A138: n <= card B1 by A16, RLAFFIN1:79;
A139: card B1 < n + 1 by A2, A135, CARD_2:67;
then card B1 <= n by NAT_1:13;
then card B1 = n by A138, XXREAL_0:1;
then card (A \ BB) = (n + 1) - n by A2, A137, CARD_2:63;
then consider ab being set such that
A140: A \ BB = {ab} by CARD_2:60;
@ U c= conv (@ U) by RLAFFIN1:2;
then A141: @ U c= conv A by A41, XBOOLE_1:1;
A142: ab in {ab} by TARSKI:def 1;
then reconsider ab = ab as Element of V by A140;
A143: conv (@ U) c= Affin (@ U) by RLAFFIN1:65;
then sum (((center_of_mass V) . U) |-- (@ U)) = 1 by A133, RLAFFIN1:def 7;
then consider F being FinSequence of REAL , G being FinSequence of the carrier of V such that
A144: ((Sum (((center_of_mass V) . U) |-- (@ U))) |-- A) . ab = Sum F and
A145: len G = len F and
G is one-to-one and
A146: rng G = Carrier (((center_of_mass V) . U) |-- (@ U)) and
A147: 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, A141, RLAFFIN2:3;
A148: dom G = dom F by A145, FINSEQ_3:31;
A149: A \ {ab} = A /\ BB by A140, XBOOLE_1:48
.= BB by A137, XBOOLE_1:28 ;
U c= conv B1

proof

A150: Carrier (((center_of_mass V) . U) |-- (@ U)) c= U by RLVECT_2:def 8;

A151: now

let i be Nat; :: thesis:
assume A152: i in dom F ; :: thesis:
A153: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A147, A152;
A154: G . i in rng G by A148, A152, FUNCT_1:def 5;
then G . i in U by A146, A150;
then A155: ((G . i) |-- A) . ab >= 0 by A7, A141, RLAFFIN1:71;
(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A146, A150, A154, RLAFFIN2:18;
hence 0 <= F . i by A153, A155; :: thesis:

end;

(center_of_mass V) . U in conv (@ S) by A132;
then A156: (center_of_mass V) . U in conv BB by A136;
assume not U c= conv B1 ; :: thesis:
then consider t being set such that
A157: t in U and
A158: not t in conv B1 by TARSKI:def 3;
U c= conv (@ U) by RLAFFIN1:2;
then A159: t in conv (@ U) by A157;
A160: (t |-- A) . ab > 0

proof

assume A161: (t |-- A) . ab <= 0 ; :: thesis:
(t |-- A) . ab >= 0 by A7, A41, A159, RLAFFIN1:71;
then for y being set st y in A \ B1 holds
(t |-- A) . y = 0 by A140, A161, TARSKI:def 1;
hence contradiction by A7, A41, A140, A149, A158, A159, RLAFFIN1:76; :: thesis:

end;

end;

then conv (@ U) c= conv B1 by CONVEX1:30;
then Affin (@ U) c= Affin B1 by RLAFFIN1:68;
hence contradiction by A130, A139, RLAFFIN1:79; :: thesis:

end;

set XX = { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } ;
A167: card { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = 2 by A16, A30, A35, A36, A130, Th43;
then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } is finite ;
then consider w1, w2 being set such that
w1 <> w2 and
A168: { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = {w1,w2} by A167, CARD_2:79;
w2 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A168, TARSKI:def 2;
then consider W2 being Simplex of n, BCS K such that
A169: w2 = W2 and
A170: 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 A168, TARSKI:def 2;
then consider W1 being Simplex of n, BCS K such that
A171: w1 = W1 and
A172: S c= W1 and
conv (@ W1) c= conv (@ U) ;
A173: W1 in X by A11, A172;
A174: X c= { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

proof

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in X ; :: thesis:
then consider W being Simplex of n, BCS K such that
A175: w = W and
A176: 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
A177: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and
card T = Z + 1 and
A178: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A27, A30, A33, A34, A176, Th41;
reconsider TS = T \/ SS1 as finite simplex-like Subset-Family of K by TOPS_2:20;
A179: W = (center_of_mass V) .: (@ TS) by A178, RELAT_1:153;
union TS in TS by A37, A177, 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 A180: card UTS <= n + 1 by A3, XXREAL_3:def 2;
A181: U c= union TS by XBOOLE_1:7, ZFMISC_1:95;
then n + 1 <= card UTS by A130, NAT_1:44;
then UTS = U by A130, A180, A181, CARD_FIN:1, XXREAL_0:1;
then conv (@ W) c= conv (@ U) by A179, 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 A175, A176; :: thesis:

end;

W2 in X by A11, A170;
then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } c= X by A168, A171, A169, A173, ZFMISC_1:38;
hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A131, A167, A174, XBOOLE_0:def 10; :: thesis:

end;