let V be RealLinearSpace; :: thesis: for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

BCS Ka is affinely-independent

let Ka be non void affinely-independent SimplicialComplex of V; :: thesis: ( |.Ka.| c= [#] Ka implies BCS Ka is affinely-independent )

set P = BCS Ka;

set B = center_of_mass V;

assume |.Ka.| c= [#] Ka ; :: thesis: BCS Ka is affinely-independent

then A1: BCS Ka = subdivision ((center_of_mass V),Ka) by Def5;

let A be Subset of (BCS Ka); :: according to SIMPLEX1:def 7 :: thesis: ( A is simplex-like implies @ A is affinely-independent )

assume A is simplex-like ; :: thesis: @ A is affinely-independent

then consider S being c=-linear finite simplex-like Subset-Family of Ka such that

A2: A = (center_of_mass V) .: S by A1, SIMPLEX0:def 20;

BCS Ka is affinely-independent

let Ka be non void affinely-independent SimplicialComplex of V; :: thesis: ( |.Ka.| c= [#] Ka implies BCS Ka is affinely-independent )

set P = BCS Ka;

set B = center_of_mass V;

assume |.Ka.| c= [#] Ka ; :: thesis: BCS Ka is affinely-independent

then A1: BCS Ka = subdivision ((center_of_mass V),Ka) by Def5;

let A be Subset of (BCS Ka); :: according to SIMPLEX1:def 7 :: thesis: ( A is simplex-like implies @ A is affinely-independent )

assume A is simplex-like ; :: thesis: @ A is affinely-independent

then consider S being c=-linear finite simplex-like Subset-Family of Ka such that

A2: A = (center_of_mass V) .: S by A1, SIMPLEX0:def 20;

per cases
( S is empty or not S is empty )
;

end;

suppose A3:
not S is empty
; :: thesis: @ A is affinely-independent

( S c= bool (union S) & bool (@ (union S)) c= bool the carrier of V )
by ZFMISC_1:67, ZFMISC_1:82;

then reconsider s = S as c=-linear finite Subset-Family of V by XBOOLE_1:1;

union S in S by A3, SIMPLEX0:9;

then union S is simplex-like by TOPS_2:def 1;

then @ (union S) is affinely-independent ;

then union s is affinely-independent ;

hence @ A is affinely-independent by A2, RLAFFIN2:29; :: thesis: verum

end;then reconsider s = S as c=-linear finite Subset-Family of V by XBOOLE_1:1;

union S in S by A3, SIMPLEX0:9;

then union S is simplex-like by TOPS_2:def 1;

then @ (union S) is affinely-independent ;

then union s is affinely-independent ;

hence @ A is affinely-independent by A2, RLAFFIN2:29; :: thesis: verum