let V be RealLinearSpace; :: thesis: for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card () holds
for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & () \/ Af is affinely-independent & () \/ Af c= Bf holds
(() .: S) \/ (() .: {(() \/ Af)}) is Simplex of card S, BCS ()

let S be finite Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card () implies for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & () \/ Af is affinely-independent & () \/ Af c= Bf holds
(() .: S) \/ (() .: {(() \/ Af)}) is Simplex of card S, BCS () )

assume that
A1: ( S is c=-linear & S is with_non-empty_elements ) and
A2: card S = card () ; :: thesis: for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & () \/ Af is affinely-independent & () \/ Af c= Bf holds
(() .: S) \/ (() .: {(() \/ Af)}) is Simplex of card S, BCS ()

set U = union S;
set b = center_of_mass V;
let A, B be finite Subset of V; :: thesis: ( not A is empty & A misses union S & () \/ A is affinely-independent & () \/ A c= B implies (() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS () )
assume that
A3: not A is empty and
A4: ( A misses union S & () \/ A is affinely-independent ) and
A5: (union S) \/ A c= B ; :: thesis: (() .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS ()
reconsider UA = () \/ A as finite Subset of V by A5;
dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
then UA in dom () by ;
then A6: {(() . UA)} = Im ((),UA) by FUNCT_1:59
.= () .: {UA} by RELAT_1:def 16 ;
set CA = Complex_of {UA};
set CB = Complex_of {B};
{UA} is_finer_than {B}
proof
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in {UA} or ex b1 being set st
( b1 in {B} & x c= b1 ) )

assume x in {UA} ; :: thesis: ex b1 being set st
( b1 in {B} & x c= b1 )

then A7: x = UA by TARSKI:def 1;
B in {B} by TARSKI:def 1;
hence ex b1 being set st
( b1 in {B} & x c= b1 ) by A5, A7; :: thesis: verum
end;
then Complex_of {UA} is SubSimplicialComplex of Complex_of {B} by SIMPLEX0:30;
then A8: subdivision ((),()) is SubSimplicialComplex of subdivision ((),()) by SIMPLEX0:58;
|.().| c= [#] () ;
then A9: subdivision ((),()) = BCS () by Def5;
|.().| c= [#] () ;
then A10: BCS () is SubSimplicialComplex of BCS () by A8, A9, Def5;
S is finite-membered
proof
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in S or x is finite )
assume x in S ; :: thesis: x is finite
then A11: x c= union S by ZFMISC_1:74;
union S is finite by A2;
hence x is finite by A11; :: thesis: verum
end;
then ((center_of_mass V) .: S) \/ (() .: {UA}) is Simplex of card S, BCS () by A1, A2, A3, A4, Lm1;
hence ((center_of_mass V) .: S) \/ (() .: {(() \/ A)}) is Simplex of card S, BCS () by ; :: thesis: verum