let V be RealLinearSpace; :: thesis:
let S be c=-linear finite finite-membered Subset-Family of V; :: thesis:
assume that
A1: S is with_non-empty_elements and
A2: (card S) + 1 = card (union S) and
A3: union S is affinely-independent ; :: thesis:
set B = center_of_mass V;
reconsider U = union S as finite affinely-independent Subset of V by A3;
reconsider s = S as Subset-Family of U by ZFMISC_1:82;
A4: not S is empty by A2, ZFMISC_1:2;
then consider ss1 being Subset-Family of U such that
A5: s c= ss1 and
A6: ( ss1 is with_non-empty_elements & ss1 is c=-linear ) and
A7: card ss1 = card U and
A8: for X being set st X in ss1 & card X <> 1 holds
ex x being set st
( x in X & X \ {x} in ss1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;
card (ss1 \ s) = ((card S) + 1) - (card S) by A2, A5, A7, CARD_2:44;
then consider x being object such that
A9: ss1 \ s = {x} by CARD_2:42;
reconsider c = card U as ExtReal ;
set CU = Complex_of {U};
set TC = the topology of (Complex_of {U});
A10: the topology of (Complex_of {U}) = bool U by SIMPLEX0:4;
then reconsider ss = ss1 as Subset-Family of (Complex_of {U}) by XBOOLE_1:1;
set BC = BCS (Complex_of {U});
reconsider cc = (card U) - 1 as ExtReal ;
A11: |.(Complex_of {U}).| c= [#] (Complex_of {U}) ;
then A12: BCS (Complex_of {U}) = subdivision ((center_of_mass V),(Complex_of {U})) by Def5;
then A13: [#] (BCS (Complex_of {U})) = [#] (Complex_of {U}) by SIMPLEX0:def 20;
then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {U})) ;
A14: ss is simplex-like

proof

let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis:
assume A in ss ; :: thesis:
hence not A is dependent by A10; :: thesis:

end;

then A15: card Bss = card U by A6, A7, Th33;
then A16: card Bss = cc + 1 by A2, XXREAL_3:def 2;
A17: x in {x} by TARSKI:def 1;
then A18: x in ss1 by A9, XBOOLE_0:def 5;
A19: not x in s by A9, A17, XBOOLE_0:def 5;
reconsider x = x as finite Subset of V by A9, A17, XBOOLE_1:1;
degree (Complex_of {U}) = c - 1 by SIMPLEX0:26
.= (card U) + (- 1) by XXREAL_3:def 2 ;
then A20: cc = degree (BCS (Complex_of {U})) by A11, Th31;
Bss is simplex-like by A6, A12, A14, SIMPLEX0:def 20;
then A21: Bss is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A16, A20, SIMPLEX0:def 18;
x <> {} by A6, A18;
then reconsider c1 = (card x) - 1 as Element of NAT by NAT_1:20;
ex xm being set st
( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )

proof

per cases ;

suppose A22: card x = 1 ; :: thesis:

then A23: ex z being object st x = {z} by CARD_2:42;
take xm = {} ; :: thesis:
thus ( ( xm in s or xm = {} ) & card xm = (card x) - 1 ) by A22; :: thesis:
let y be set ; :: thesis:
assume that
A24: y in s and
A25: y c= x ; :: thesis:
y <> x by A9, A17, A24, XBOOLE_0:def 5;
hence y c= xm by A23, A25, ZFMISC_1:33; :: thesis:

end;

suppose card x <> 1 ; :: thesis:

then consider z being set such that
A26: z in x and
A27: x \ {z} in ss1 by A8, A18;
take xm = x \ {z}; :: thesis:
A28: x = xm \/ {z} by A26, ZFMISC_1:116;
xm in s

proof

assume not xm in s ; :: thesis:
then xm in ss1 \ s by A27, XBOOLE_0:def 5;
then xm = x by A9, TARSKI:def 1;
hence contradiction by A26, ZFMISC_1:56; :: thesis:

end;

hence ( xm in s or xm = {} ) ; :: thesis:
card x = c1 + 1 ;
hence card xm = (card x) - 1 by A26, STIRL2_1:55; :: thesis:
let y be set ; :: thesis:
assume that
A29: y in s and
A30: y c= x ; :: thesis:
assume A31: not y c= xm ; :: thesis:
xm,y are_c=-comparable by A5, A6, A27, A29;
then xm c= y by A31;
hence contradiction by A19, A28, A29, A30, A31, ZFMISC_1:138; :: thesis:

end;

then consider xm being set such that
A32: ( xm in s or xm = {} ) and
A33: card xm = (card x) - 1 and
A34: for y being set st y in s & y c= x holds
y c= xm ;
A35: U in S by A4, SIMPLEX0:9;
then ( union ss1 c= U & U c= union ss ) by A5, ZFMISC_1:74;
then A36: union ss = U ;
x c< U by A9, A17, A19, A35;
then card x < card U by CARD_2:48;
then (card x) + 1 <= card U by NAT_1:13;
then consider xM being set such that
A37: xM in ss and
A38: card xM = (card x) + 1 by A6, A36, A21, Th36;
reconsider xm = xm as finite Subset of V by A32, XBOOLE_1:2;
reconsider xM = xM as finite Subset of V by A37;
A39: not xM c= xm

proof

assume xM c= xm ; :: thesis:
then (card x) + 1 <= (card x) + (- 1) by A33, A38, NAT_1:43;
hence contradiction by XREAL_1:6; :: thesis:

end;

A40: xM in s

proof

assume not xM in s ; :: thesis:
then xM in ss \ s by A37, XBOOLE_0:def 5;
then xM = x by A9, TARSKI:def 1;
hence contradiction by A38; :: thesis:

end;

then ( xm,xM are_c=-comparable or xm c= xM ) by A32, ORDINAL1:def 8;
then A41: xm c= xM by A39;
then card (xM \ xm) = (card xM) - (card xm) by CARD_2:44;
then consider x1, x2 being object such that
A42: x1 <> x2 and
A43: xM \ xm = {x1,x2} by A33, A38, CARD_2:60;
A44: x1 in {x1,x2} by TARSKI:def 2;
A45: x2 in {x1,x2} by TARSKI:def 2;
then reconsider x1 = x1, x2 = x2 as Element of V by A43, A44;
set xm1 = xm \/ {x1};
set xm2 = xm \/ {x2};
reconsider S1 = S \/ {(xm \/ {x1})}, S2 = S \/ {(xm \/ {x2})} as Subset-Family of (Complex_of {U}) ;
reconsider BS1 = (center_of_mass V) .: S1, BS2 = (center_of_mass V) .: S2 as Subset of (BCS (Complex_of {U})) by A13;
A46: BS1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by RELAT_1:120;
A47: not x1 in xm by A43, A44, XBOOLE_0:def 5;
then A48: card (xm \/ {x1}) = (card xm) + 1 by CARD_2:41;
A49: not xm \/ {x1} in S

proof

assume A50: xm \/ {x1} in S ; :: thesis:
then x,xm \/ {x1} are_c=-comparable by A5, A6, A18;
then ( x c= xm \/ {x1} or xm \/ {x1} c= x ) ;
hence contradiction by A19, A33, A48, A50, CARD_2:102; :: thesis:

end;

not x2 in xm by A43, A45, XBOOLE_0:def 5;
then A51: card (xm \/ {x2}) = (card xm) + 1 by CARD_2:41;
A52: not xm \/ {x2} in S

proof

assume A53: xm \/ {x2} in S ; :: thesis:
then x,xm \/ {x2} are_c=-comparable by A5, A6, A18;
then ( x c= xm \/ {x2} or xm \/ {x2} c= x ) ;
hence contradiction by A19, A33, A51, A53, CARD_2:102; :: thesis:

end;

x2 in xM by A43, A45, XBOOLE_0:def 5;
then {x2} c= xM by ZFMISC_1:31;
then A54: xm \/ {x2} c= xM by A41, XBOOLE_1:8;
A55: S2 c= bool U

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A56: A in S2 ; :: thesis:
reconsider AA = A as set by TARSKI:1;

per cases by A56, XBOOLE_0:def 3;

suppose A in S ; :: thesis:

then AA c= U by ZFMISC_1:74;
hence A in bool U ; :: thesis:

end;

suppose A in {(xm \/ {x2})} ; :: thesis:

then A = xm \/ {x2} by TARSKI:def 1;
then AA c= U by A37, A54, XBOOLE_1:1;
hence A in bool U ; :: thesis:

end;

A57: S2 is simplex-like

proof

let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis:
assume A in S2 ; :: thesis:
hence not A is dependent by A10, A55; :: thesis:

end;

then card BS2 = card S2 by A1, Th33;
then A58: card BS2 = (card S) + 1 by A52, CARD_2:41;
x1 in xM by A43, A44, XBOOLE_0:def 5;
then {x1} c= xM by ZFMISC_1:31;
then A59: xm \/ {x1} c= xM by A41, XBOOLE_1:8;
A60: S1 c= bool U

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A61: A in S1 ; :: thesis:
reconsider AA = A as set by TARSKI:1;

per cases by A61, XBOOLE_0:def 3;

suppose A in S ; :: thesis:

then AA c= U by ZFMISC_1:74;
hence A in bool U ; :: thesis:

end;

suppose A in {(xm \/ {x1})} ; :: thesis:

then A = xm \/ {x1} by TARSKI:def 1;
then AA c= U by A37, A59, XBOOLE_1:1;
hence A in bool U ; :: thesis:

end;

then A62: BS1 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S1 by A10, RELAT_1:129;
A63: S1 is simplex-like

proof

let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis:
assume A in S1 ; :: thesis:
hence not A is dependent by A10, A60; :: thesis:

end;

then card BS1 = card S1 by A1, Th33;
then A64: card BS1 = (card S) + 1 by A49, CARD_2:41;
A65: ( xm c= xm \/ {x1} & xm c= xm \/ {x2} ) by XBOOLE_1:7;
A66: for y1 being set st y1 in S holds
( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

proof

let y1 be set ; :: thesis:
assume A67: y1 in S ; :: thesis:
then A68: xM,y1 are_c=-comparable by A40, ORDINAL1:def 8;

per cases by A68;

suppose ( xM c= y1 or xM = y1 ) ; :: thesis:

then ( xm \/ {x1} c= y1 & xm \/ {x2} c= y1 ) by A54, A59;
hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis:

end;

suppose A69: ( y1 c= xM & xM <> y1 ) ; :: thesis:

then reconsider y1 = y1 as finite set ;
A70: y1 c< xM by A69;
A71: not x c= y1

proof

A72: card y1 < card xM by A70, CARD_2:48;
assume A73: x c= y1 ; :: thesis:
then card x <= card y1 by NAT_1:43;
then card x = card y1 by A38, A72, NAT_1:9;
hence contradiction by A19, A67, A73, CARD_2:102; :: thesis:

end;

x in ss by A9, A17, XBOOLE_0:def 5;
then y1,x are_c=-comparable by A5, A6, A67;
then y1 c= x by A71;
then y1 c= xm by A34, A67;
then ( y1 c= xm \/ {x1} & y1 c= xm \/ {x2} ) by A65;
hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis:

end;

S1 is c=-linear

proof

let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis:
assume that
A74: y1 in S1 and
A75: y2 in S1 ; :: thesis:
( y1 in S or y1 in {(xm \/ {x1})} ) by A74, XBOOLE_0:def 3;
then A76: ( y1 in S or y1 = xm \/ {x1} ) by TARSKI:def 1;
( y2 in S or y2 in {(xm \/ {x1})} ) by A75, XBOOLE_0:def 3;
then ( y2 in S or y2 = xm \/ {x1} ) by TARSKI:def 1;
hence y1,y2 are_c=-comparable by A66, A76, ORDINAL1:def 8; :: thesis:

end;

then BS1 is simplex-like by A12, A63, SIMPLEX0:def 20;
then A77: BS1 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A64, SIMPLEX0:def 18;
set SS = { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ;
(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by XBOOLE_1:7;
then A78: BS1 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A46, A77;
A79: BS2 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by RELAT_1:120;
A80: { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } c= {BS1,BS2}

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
reconsider n = 0 as Nat ;
assume w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ; :: thesis:
then consider W being Simplex of card S, BCS (Complex_of {U}) such that
A81: w = W and
A82: (center_of_mass V) .: S c= W ;
((card S) + n) + 1 <= card U by A2;
then consider T being finite Subset-Family of V such that
A83: T misses S and
A84: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and
A85: card T = n + 1 and
A86: union T c= U and
A87: @ W = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A1, A82, Th35;
consider x3 being object such that
A88: {x3} = T by A85, CARD_2:42;
A89: x3 in T by A88, TARSKI:def 1;
then A90: not x3 in S by A83, XBOOLE_0:3;
reconsider x3 = x3 as set by TARSKI:1;
A91: x3 c= union T by A89, ZFMISC_1:74;
A92: x3 in T \/ S by A89, XBOOLE_0:def 3;
reconsider x3 = x3 as finite Subset of U by A86, A91, XBOOLE_1:1;
A93: not xM c= x3

proof

consider x4 being set such that
A94: x4 in ss and
A95: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;
assume xM c= x3 ; :: thesis:
then (card x) + 1 <= card x3 by A38, NAT_1:43;
then x <> x4 by A95, NAT_1:13;
then not x4 in {x} by TARSKI:def 1;
then A96: x4 in s by A9, A94, XBOOLE_0:def 5;
then x4 in S \/ T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by A84, A92;
then ( x3 c= x4 or x4 c= x3 ) ;
hence contradiction by A90, A95, A96, CARD_2:102; :: thesis:

end;

A97: ( xm c= x3 & xm <> x3 )

proof

per cases by A32;

suppose xm = {} ; :: thesis:

hence ( xm c= x3 & xm <> x3 ) by A84, A92; :: thesis:

end;

suppose A98: xm in s ; :: thesis:

A99: not x3 c= xm

proof

assume x3 c= xm ; :: thesis:
then A100: card x3 <= card xm by NAT_1:43;
consider x4 being set such that
A101: x4 in ss and
A102: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;
(card xm) + 1 = card x by A33;
then card x <> card x3 by A100, NAT_1:13;
then not x4 in {x} by A102, TARSKI:def 1;
then A103: x4 in s by A9, A101, XBOOLE_0:def 5;
then x4 in S \/ T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by A84, A92;
then ( x3 c= x4 or x4 c= x3 ) ;
hence contradiction by A90, A102, A103, CARD_2:102; :: thesis:

end;

xm in T \/ S by A98, XBOOLE_0:def 3;
then xm,x3 are_c=-comparable by A84, A92;
hence ( xm c= x3 & xm <> x3 ) by A99; :: thesis:

end;

then A104: x3 = x3 \/ xm by XBOOLE_1:12;
xM in S \/ T by A40, XBOOLE_0:def 3;
then xM,x3 are_c=-comparable by A84, A92;
then x3 c= xM by A93;
then A105: x3 \ xm c= xM \ xm by XBOOLE_1:33;
A106: xM = xm \/ xM by A41, XBOOLE_1:12;
A107: x3 \ xm <> xM \ xm

proof

assume x3 \ xm = xM \ xm ; :: thesis:
then x3 = (xM \ xm) \/ xm by A104, XBOOLE_1:39;
hence contradiction by A93, A106, XBOOLE_1:39; :: thesis:

end;

A108: x3 \ xm <> {} by XBOOLE_1:37, A97;
x3 \/ xm = (x3 \ xm) \/ xm by XBOOLE_1:39;
then ( x3 = xm \/ {x1} or x3 = xm \/ {x2} ) by A43, A104, A105, A107, A108, ZFMISC_1:36;
hence w in {BS1,BS2} by A79, A46, A81, A87, A88, TARSKI:def 2; :: thesis:

end;

A109: BS2 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S2 by A10, A55, RELAT_1:129;
A110: BS1 <> BS2

proof

end;

S2 is c=-linear

proof

let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis:
assume that
A123: y1 in S2 and
A124: y2 in S2 ; :: thesis:
( y1 in S or y1 in {(xm \/ {x2})} ) by A123, XBOOLE_0:def 3;
then A125: ( y1 in S or y1 = xm \/ {x2} ) by TARSKI:def 1;
( y2 in S or y2 in {(xm \/ {x2})} ) by A124, XBOOLE_0:def 3;
then ( y2 in S or y2 = xm \/ {x2} ) by TARSKI:def 1;
hence y1,y2 are_c=-comparable by A66, A125, ORDINAL1:def 8; :: thesis:

end;

then BS2 is simplex-like by A12, A57, SIMPLEX0:def 20;
then A126: BS2 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A58, SIMPLEX0:def 18;
(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by XBOOLE_1:7;
then BS2 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A79, A126;
then {BS1,BS2} c= { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A78, ZFMISC_1:32;
then { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } = {BS1,BS2} by A80;
hence card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 by A110, CARD_2:57; :: thesis: