let V be RealLinearSpace; :: thesis: for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})
let S be finite finite-membered Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )
assume that
A1: S is c=-linear and
A2: S is with_non-empty_elements and
A3: card S = card (union S) ; :: thesis: for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})
set U = union S;
set B = center_of_mass V;
let A be non empty finite Subset of V; :: thesis: ( A misses union S & (union S) \/ A is affinely-independent implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )
assume that
A4: A misses union S and
A5: (union S) \/ A is affinely-independent ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})
reconsider UA = (union S) \/ A as finite affinely-independent Subset of V by A5;
set C = Complex_of {UA};
reconsider SUA = S \/ {UA} as Subset-Family of (Complex_of {UA}) ;
A6: union S c= UA by XBOOLE_1:7;
A7: the topology of (Complex_of {UA}) = bool UA by SIMPLEX0:4;
A8: SUA c= the topology of (Complex_of {UA})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SUA or x in the topology of (Complex_of {UA}) )
reconsider xx = x as set by TARSKI:1;
assume x in SUA ; :: thesis: x in the topology of (Complex_of {UA})
then ( x in S or x in {UA} ) by XBOOLE_0:def 3;
then ( xx c= union S or x = UA ) by TARSKI:def 1, ZFMISC_1:74;
then xx c= UA by A6;
hence x in the topology of (Complex_of {UA}) by A7; :: thesis: verum

end;

A9: SUA is simplex-like

proof

let A be Subset of (Complex_of {UA}); :: according to TOPS_2:def 1 :: thesis: ( not A in SUA or not A is dependent )
assume A in SUA ; :: thesis: not A is dependent
hence not A is dependent by A8; :: thesis: verum

end;

set BC = BCS (Complex_of {UA});
A10: |.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;
then A11: BCS (Complex_of {UA}) = subdivision ((center_of_mass V),(Complex_of {UA})) by Def5;
then [#] (BCS (Complex_of {UA})) = [#] (Complex_of {UA}) by SIMPLEX0:def 20;
then reconsider BSUA = (center_of_mass V) .: SUA as Subset of (BCS (Complex_of {UA})) ;
SUA is c=-linear

proof

let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x in SUA or not y in SUA or x,y are_c=-comparable )
assume A12: ( x in SUA & y in SUA ) ; :: thesis: x,y are_c=-comparable

per cases ( ( x in S & y in S ) or ( x in S & y in {UA} ) or ( x in {UA} & y in S ) or ( x in {UA} & y in {UA} ) ) by A12, XBOOLE_0:def 3;

suppose ( x in S & y in S ) ; :: thesis: x,y are_c=-comparable

hence x,y are_c=-comparable by A1; :: thesis: verum

end;

suppose ( x in S & y in {UA} ) ; :: thesis: x,y are_c=-comparable

then ( x c= union S & y = UA ) by TARSKI:def 1, ZFMISC_1:74;
then x c= y by A6;
hence x,y are_c=-comparable ; :: thesis: verum

end;

suppose ( x in {UA} & y in S ) ; :: thesis: x,y are_c=-comparable

then ( x = UA & y c= union S ) by TARSKI:def 1, ZFMISC_1:74;
then y c= x by A6;
hence x,y are_c=-comparable ; :: thesis: verum

end;

suppose A13: ( x in {UA} & y in {UA} ) ; :: thesis: x,y are_c=-comparable

then x = UA by TARSKI:def 1;
hence x,y are_c=-comparable by A13, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then reconsider BSUA = BSUA as Simplex of (BCS (Complex_of {UA})) by A9, A11, SIMPLEX0:def 20;
reconsider c = card UA as ExtReal ;
A14: degree (Complex_of {UA}) = c - 1 by SIMPLEX0:26
.= (card UA) + (- 1) by XXREAL_3:def 2 ;
A15: UA <> union S

proof

assume UA = union S ; :: thesis: contradiction
then A c= union S by XBOOLE_1:7;
hence contradiction by A4, XBOOLE_1:67; :: thesis: verum

end;

not UA in S by ZFMISC_1:74, A6, A15;
then A16: card SUA = (card S) + 1 by CARD_2:41;
union S c< UA by A6, A15;
then card (union S) < card UA by CARD_2:48;
then (card (union S)) + 1 <= card UA by NAT_1:13;
then A17: card (union S) <= (card UA) - 1 by XREAL_1:19;
reconsider c = card S as ExtReal ;
card BSUA = card SUA by A2, A9, Th33;
then A18: card BSUA = c + 1 by A16, XXREAL_3:def 2;
degree (BCS (Complex_of {UA})) = degree (Complex_of {UA}) by A10, Th31;
then BSUA is Simplex of card S, BCS (Complex_of {UA}) by A3, A14, A17, A18, SIMPLEX0:def 18;
hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) by RELAT_1:120; :: thesis: verum