let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ) holds
degree Kv = degree (BCS Kv)

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ) implies degree Kv = degree (BCS Kv) )

assume that
A1: |.Kv.| c= [#] Kv and
A2: for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ; :: thesis: degree Kv = degree (BCS Kv)
A3: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
A4: for n being Nat st n <= degree Kv holds
ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom () & () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one )
proof
let n be Nat; :: thesis: ( n <= degree Kv implies ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom () & () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one ) )

assume n <= degree Kv ; :: thesis: ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom () & () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one )

then consider S being Simplex of Kv such that
A5: card S = n + 1 and
A6: @ S is affinely-independent by A2;
take S ; :: thesis: ( S is simplex-like & card S = n + 1 & BOOL S c= dom () & () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one )
thus ( S is simplex-like & card S = n + 1 ) by A5; :: thesis: ( BOOL S c= dom () & () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one )
A7: the topology of (Complex_of {(@ S)}) = bool S by SIMPLEX0:4;
reconsider SS = {(@ S)} as affinely-independent Subset-Family of V by A6;
A8: (center_of_mass V) .: (BOOL S) c= conv (@ S)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in () .: (BOOL S) or y in conv (@ S) )
assume y in () .: (BOOL S) ; :: thesis: y in conv (@ S)
then consider x being object such that
A9: x in dom () and
A10: ( x in BOOL S & () . x = y ) by FUNCT_1:def 6;
reconsider x = x as non empty Subset of V by ;
( conv x c= conv (@ S) & y in conv x ) by ;
hence y in conv (@ S) ; :: thesis: verum
end;
bool (@ S) c= bool the carrier of V by ZFMISC_1:67;
hence BOOL S c= dom () by ; :: thesis: ( () .: (BOOL S) is Subset of Kv & () | (BOOL S) is one-to-one )
conv (@ S) c= |.Kv.| by Th5;
then conv (@ S) c= [#] Kv by A1;
hence (center_of_mass V) .: (BOOL S) is Subset of Kv by ; :: thesis: () | (BOOL S) is one-to-one
( ((center_of_mass V) | (bool S)) | (BOOL S) = () | (BOOL S) & Complex_of SS is SimplicialComplex of V ) by RELAT_1:74;
hence (center_of_mass V) | (BOOL S) is one-to-one by ; :: thesis: verum
end;
not {} in dom () by ZFMISC_1:56;
then A11: dom () is with_non-empty_elements ;
BCS Kv = subdivision ((),Kv) by ;
hence degree Kv = degree (BCS Kv) by ; :: thesis: verum