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