let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS 1,Kv = BCS Kv
let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv implies BCS 1,Kv = BCS Kv )
assume A1: |.Kv.| c= [#] Kv ; :: thesis: BCS 1,Kv = BCS Kv
hence BCS 1,Kv = subdivision 1,(center_of_mass V),Kv by Def6
.= subdivision (center_of_mass V),Kv by SIMPLEX0:62
.= BCS Kv by A1, Def5 ;
:: thesis: verum