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 () holds
for A being non empty finite Subset of V st A misses union S & () \/ A is affinely-independent holds
(() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ 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 () implies for A being non empty finite Subset of V st A misses union S & () \/ A is affinely-independent holds
(() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ A)}) )

assume that
A1: S is c=-linear and
A2: S is with_non-empty_elements and
A3: card S = card () ; :: thesis: for A being non empty finite Subset of V st A misses union S & () \/ A is affinely-independent holds
(() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ 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 & () \/ A is affinely-independent implies (() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ A)}) )
assume that
A4: A misses union S and
A5: (union S) \/ A is affinely-independent ; :: thesis: (() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ A)})
reconsider UA = () \/ A as finite affinely-independent Subset of V by A5;
set C = Complex_of {UA};
reconsider SUA = S \/ {UA} as Subset-Family of () ;
A6: union S c= UA by XBOOLE_1:7;
A7: the topology of () = bool UA by SIMPLEX0:4;
A8: SUA c= the topology of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SUA or x in the topology of () )
reconsider xx = x as set by TARSKI:1;
assume x in SUA ; :: thesis: x in the topology of ()
then ( x in S or x in {UA} ) by XBOOLE_0:def 3;
then ( xx c= union S or x = UA ) by ;
then xx c= UA by A6;
hence x in the topology of () by A7; :: thesis: verum
end;
A9: SUA is simplex-like
proof
let A be Subset of (); :: 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 ();
A10: |.().| c= [#] () ;
then A11: BCS () = subdivision ((),()) by Def5;
then [#] (BCS ()) = [#] () by SIMPLEX0:def 20;
then reconsider BSUA = () .: SUA as Subset of (BCS ()) ;
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:
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 ;
end;
end;
then reconsider BSUA = BSUA as Simplex of (BCS ()) by ;
reconsider c = card UA as ExtReal ;
A14: degree () = c - 1 by SIMPLEX0:26
.= (card UA) + (- 1) by XXREAL_3:def 2 ;
A15: UA <> union S
proof end;
not UA in S by ;
then A16: card SUA = (card S) + 1 by CARD_2:41;
union S c< UA by ;
then card () < card UA by CARD_2:48;
then (card ()) + 1 <= card UA by NAT_1:13;
then A17: card () <= (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 ;
degree (BCS ()) = degree () by ;
then BSUA is Simplex of card S, BCS () by ;
hence ((center_of_mass V) .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS (Complex_of {(() \/ A)}) by RELAT_1:120; :: thesis: verum