let V be RealLinearSpace; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & (card Sf) + 1 = card (union Sf) & union Sf is affinely-independent holds
card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : () .: Sf c= S1 } = 2

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & (card S) + 1 = card () & union S is affinely-independent implies card { S1 where S1 is Simplex of card S, BCS () : () .: S c= S1 } = 2 )
assume that
A1: S is with_non-empty_elements and
A2: (card S) + 1 = card () and
A3: union S is affinely-independent ; :: thesis: card { S1 where S1 is Simplex of card S, BCS () : () .: S c= S1 } = 2
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 ;
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 ;
card (ss1 \ s) = ((card S) + 1) - (card S) by ;
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 ();
A10: the topology of () = bool U by SIMPLEX0:4;
then reconsider ss = ss1 as Subset-Family of () by XBOOLE_1:1;
set BC = BCS ();
reconsider cc = (card U) - 1 as ExtReal ;
A11: |.().| c= [#] () ;
then A12: BCS () = subdivision ((),()) by Def5;
then A13: [#] (BCS ()) = [#] () by SIMPLEX0:def 20;
then reconsider Bss = () .: ss as Subset of (BCS ()) ;
A14: ss is simplex-like
proof
let A be Subset of (); :: according to TOPS_2:def 1 :: thesis: ( not A in ss or not A is dependent )
assume A in ss ; :: thesis: not A is dependent
hence not A is dependent by A10; :: thesis: verum
end;
then A15: card Bss = card U by A6, A7, Th33;
then A16: card Bss = cc + 1 by ;
A17: x in {x} by TARSKI:def 1;
then A18: x in ss1 by ;
A19: not x in s by ;
reconsider x = x as finite Subset of V by ;
degree () = c - 1 by SIMPLEX0:26
.= (card U) + (- 1) by XXREAL_3:def 2 ;
then A20: cc = degree (BCS ()) by ;
Bss is simplex-like by ;
then A21: Bss is Simplex of (card U) - 1, BCS () by ;
x <> {} by ;
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 ( card x = 1 or card x <> 1 ) ;
suppose A22: card x = 1 ; :: thesis: 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 ) )

then A23: ex z being object st x = {z} by CARD_2:42;
take xm = {} ; :: thesis: ( ( 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 ) )

thus ( ( xm in s or xm = {} ) & card xm = (card x) - 1 ) by A22; :: thesis: for y being set st y in s & y c= x holds
y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )
assume that
A24: y in s and
A25: y c= x ; :: thesis: y c= xm
y <> x by ;
hence y c= xm by ; :: thesis: verum
end;
suppose card x <> 1 ; :: thesis: 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 ) )

then consider z being set such that
A26: z in x and
A27: x \ {z} in ss1 by ;
take xm = x \ {z}; :: thesis: ( ( 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 ) )

A28: x = xm \/ {z} by ;
xm in s
proof
assume not xm in s ; :: thesis: contradiction
then xm in ss1 \ s by ;
then xm = x by ;
hence contradiction by A26, ZFMISC_1:56; :: thesis: verum
end;
hence ( xm in s or xm = {} ) ; :: thesis: ( card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )

card x = c1 + 1 ;
hence card xm = (card x) - 1 by ; :: thesis: for y being set st y in s & y c= x holds
y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )
assume that
A29: y in s and
A30: y c= x ; :: thesis: y c= xm
assume A31: not y c= xm ; :: thesis: contradiction
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: verum
end;
end;
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 ;
then ( union ss1 c= U & U c= union ss ) by ;
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 ;
reconsider xM = xM as finite Subset of V by A37;
A39: not xM c= xm
proof
assume xM c= xm ; :: thesis: contradiction
then (card x) + 1 <= (card x) + (- 1) by ;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
A40: xM in s
proof
assume not xM in s ; :: thesis: contradiction
then xM in ss \ s by ;
then xM = x by ;
hence contradiction by A38; :: thesis: verum
end;
then ( xm,xM are_c=-comparable or xm c= xM ) by ;
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 ;
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 ;
set xm1 = xm \/ {x1};
set xm2 = xm \/ {x2};
reconsider S1 = S \/ {(xm \/ {x1})}, S2 = S \/ {(xm \/ {x2})} as Subset-Family of () ;
reconsider BS1 = () .: S1, BS2 = () .: S2 as Subset of (BCS ()) by A13;
A46: BS1 = (() .: S) \/ (() .: {(xm \/ {x1})}) by RELAT_1:120;
A47: not x1 in xm by ;
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: contradiction
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: verum
end;
not x2 in xm by ;
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: contradiction
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: verum
end;
x2 in xM by ;
then {x2} c= xM by ZFMISC_1:31;
then A54: xm \/ {x2} c= xM by ;
A55: S2 c= bool U
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in S2 or A in bool U )
assume A56: A in S2 ; :: thesis: A in bool U
reconsider AA = A as set by TARSKI:1;
per cases ( A in S or A in {(xm \/ {x2})} ) by ;
end;
end;
A57: S2 is simplex-like
proof
let A be Subset of (); :: according to TOPS_2:def 1 :: thesis: ( not A in S2 or not A is dependent )
assume A in S2 ; :: thesis: not A is dependent
hence not A is dependent by ; :: thesis: verum
end;
then card BS2 = card S2 by ;
then A58: card BS2 = (card S) + 1 by ;
x1 in xM by ;
then {x1} c= xM by ZFMISC_1:31;
then A59: xm \/ {x1} c= xM by ;
A60: S1 c= bool U
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in S1 or A in bool U )
assume A61: A in S1 ; :: thesis: A in bool U
reconsider AA = A as set by TARSKI:1;
per cases ( A in S or A in {(xm \/ {x1})} ) by ;
end;
end;
then A62: BS1 = (() | the topology of ()) .: S1 by ;
A63: S1 is simplex-like
proof
let A be Subset of (); :: according to TOPS_2:def 1 :: thesis: ( not A in S1 or not A is dependent )
assume A in S1 ; :: thesis: not A is dependent
hence not A is dependent by ; :: thesis: verum
end;
then card BS1 = card S1 by ;
then A64: card BS1 = (card S) + 1 by ;
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: ( y1 in S implies ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) )
assume A67: y1 in S ; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )
then A68: xM,y1 are_c=-comparable by ;
per cases ( xM c= y1 or xM = y1 or ( y1 c= xM & xM <> y1 ) ) by A68;
suppose ( xM c= y1 or xM = y1 ) ; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )
then ( xm \/ {x1} c= y1 & xm \/ {x2} c= y1 ) by ;
hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis: verum
end;
suppose A69: ( y1 c= xM & xM <> y1 ) ; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )
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 ;
assume A73: x c= y1 ; :: thesis: contradiction
then card x <= card y1 by NAT_1:43;
then card x = card y1 by ;
hence contradiction by A19, A67, A73, CARD_2:102; :: thesis: verum
end;
x in ss by ;
then y1,x are_c=-comparable by A5, A6, A67;
then y1 c= x by A71;
then y1 c= xm by ;
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: verum
end;
end;
end;
S1 is c=-linear
proof
let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not y1 in S1 or not y2 in S1 or y1,y2 are_c=-comparable )
assume that
A74: y1 in S1 and
A75: y2 in S1 ; :: thesis: y1,y2 are_c=-comparable
( y1 in S or y1 in {(xm \/ {x1})} ) by ;
then A76: ( y1 in S or y1 = xm \/ {x1} ) by TARSKI:def 1;
( y2 in S or y2 in {(xm \/ {x1})} ) by ;
then ( y2 in S or y2 = xm \/ {x1} ) by TARSKI:def 1;
hence y1,y2 are_c=-comparable by ; :: thesis: verum
end;
then BS1 is simplex-like by ;
then A77: BS1 is Simplex of (card U) - 1, BCS () by ;
set SS = { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } ;
(center_of_mass V) .: S c= (() .: S) \/ (() .: {(xm \/ {x1})}) by XBOOLE_1:7;
then A78: BS1 in { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } by A2, A46, A77;
A79: BS2 = (() .: S) \/ (() .: {(xm \/ {x2})}) by RELAT_1:120;
A80: { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } c= {BS1,BS2}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } or w in {BS1,BS2} )
reconsider n = 0 as Nat ;
assume w in { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } ; :: thesis: w in {BS1,BS2}
then consider W being Simplex of card S, BCS () 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 = (() .: S) \/ (() .: T) by ;
consider x3 being object such that
A88: {x3} = T by ;
A89: x3 in T by ;
then A90: not x3 in S by ;
reconsider x3 = x3 as set by TARSKI:1;
A91: x3 c= union T by ;
A92: x3 in T \/ S by ;
reconsider x3 = x3 as finite Subset of U by ;
A93: not xM c= x3
proof
consider x4 being set such that
A94: x4 in ss and
A95: card x4 = card x3 by ;
assume xM c= x3 ; :: thesis: contradiction
then (card x) + 1 <= card x3 by ;
then x <> x4 by ;
then not x4 in {x} by TARSKI:def 1;
then A96: x4 in s by ;
then x4 in S \/ T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by ;
then ( x3 c= x4 or x4 c= x3 ) ;
hence contradiction by A90, A95, A96, CARD_2:102; :: thesis: verum
end;
A97: ( xm c= x3 & xm <> x3 )
proof
per cases ( xm = {} or xm in s ) by A32;
suppose xm = {} ; :: thesis: ( xm c= x3 & xm <> x3 )
hence ( xm c= x3 & xm <> x3 ) by ; :: thesis: verum
end;
suppose A98: xm in s ; :: thesis: ( xm c= x3 & xm <> x3 )
A99: not x3 c= xm
proof
assume x3 c= xm ; :: thesis: contradiction
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 ;
(card xm) + 1 = card x by A33;
then card x <> card x3 by ;
then not x4 in {x} by ;
then A103: x4 in s by ;
then x4 in S \/ T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by ;
then ( x3 c= x4 or x4 c= x3 ) ;
hence contradiction by A90, A102, A103, CARD_2:102; :: thesis: verum
end;
xm in T \/ S by ;
then xm,x3 are_c=-comparable by ;
hence ( xm c= x3 & xm <> x3 ) by A99; :: thesis: verum
end;
end;
end;
then A104: x3 = x3 \/ xm by XBOOLE_1:12;
xM in S \/ T by ;
then xM,x3 are_c=-comparable by ;
then x3 c= xM by A93;
then A105: x3 \ xm c= xM \ xm by XBOOLE_1:33;
A106: xM = xm \/ xM by ;
A107: x3 \ xm <> xM \ xm
proof
assume x3 \ xm = xM \ xm ; :: thesis: contradiction
then x3 = (xM \ xm) \/ xm by ;
hence contradiction by A93, A106, XBOOLE_1:39; :: thesis: verum
end;
A108: x3 \ xm <> {} by ;
x3 \/ xm = (x3 \ xm) \/ xm by XBOOLE_1:39;
then ( x3 = xm \/ {x1} or x3 = xm \/ {x2} ) by ;
hence w in {BS1,BS2} by ; :: thesis: verum
end;
A109: BS2 = (() | the topology of ()) .: S2 by ;
A110: BS1 <> BS2
proof
assume A111: BS1 = BS2 ; :: thesis: contradiction
then BS1 \ BS2 = {} by XBOOLE_1:37;
then ((center_of_mass V) | the topology of ()) .: (S1 \ S2) = {} by ;
then A112: dom (() | the topology of ()) misses S1 \ S2 by RELAT_1:118;
BS2 \ BS1 = {} by ;
then ((center_of_mass V) | the topology of ()) .: (S2 \ S1) = {} by ;
then A113: dom (() | the topology of ()) misses S2 \ S1 by RELAT_1:118;
A114: dom (() | the topology of ()) = () /\ the topology of () by RELAT_1:61;
xm \/ {x1} in {(xm \/ {x1})} by TARSKI:def 1;
then A115: xm \/ {x1} in S1 by XBOOLE_0:def 3;
A116: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
A117: S1 \ S2 c= S1 by XBOOLE_1:36;
then not {} in S1 \ S2 by A1;
then A118: S1 \ S2 c= dom () by ;
A119: S2 \ S1 c= S2 by XBOOLE_1:36;
then not {} in S2 \ S1 by A1;
then A120: S2 \ S1 c= dom () by ;
S1 \ S2 c= bool U by ;
then S1 \ S2 c= dom (() | the topology of ()) by ;
then A121: S1 \ S2 = {} by ;
S2 \ S1 c= bool U by ;
then S2 \ S1 c= dom (() | the topology of ()) by ;
then S1 = S2 by ;
then xm \/ {x1} in {(xm \/ {x2})} by ;
then A122: xm \/ {x1} = xm \/ {x2} by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then x1 in xm \/ {x1} by XBOOLE_0:def 3;
then x1 in {x2} by ;
hence contradiction by A42, TARSKI:def 1; :: thesis: verum
end;
S2 is c=-linear
proof
let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not y1 in S2 or not y2 in S2 or y1,y2 are_c=-comparable )
assume that
A123: y1 in S2 and
A124: y2 in S2 ; :: thesis: y1,y2 are_c=-comparable
( y1 in S or y1 in {(xm \/ {x2})} ) by ;
then A125: ( y1 in S or y1 = xm \/ {x2} ) by TARSKI:def 1;
( y2 in S or y2 in {(xm \/ {x2})} ) by ;
then ( y2 in S or y2 = xm \/ {x2} ) by TARSKI:def 1;
hence y1,y2 are_c=-comparable by ; :: thesis: verum
end;
then BS2 is simplex-like by ;
then A126: BS2 is Simplex of (card U) - 1, BCS () by ;
(center_of_mass V) .: S c= (() .: S) \/ (() .: {(xm \/ {x2})}) by XBOOLE_1:7;
then BS2 in { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } by ;
then {BS1,BS2} c= { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } by ;
then { S3 where S3 is Simplex of card S, BCS () : () .: S c= S3 } = {BS1,BS2} by A80;
hence card { S1 where S1 is Simplex of card S, BCS () : () .: S c= S1 } = 2 by ; :: thesis: verum