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