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;
per cases ( S is empty or not S is empty ) ;
suppose S is empty ; :: thesis: @ A is affinely-independent
then A = {} by A2;
hence @ A is affinely-independent ; :: thesis: verum
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;
end;