let n be Nat; :: thesis: for V being RealLinearSpace
for Kv being non void SimplicialComplex of V
for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv & |.Sv.| c= [#] Sv holds
BCS n,Sv is SubSimplicialComplex of BCS n,Kv
let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V
for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv & |.Sv.| c= [#] Sv holds
BCS n,Sv is SubSimplicialComplex of BCS n,Kv
let Kv be non void SimplicialComplex of V; :: thesis: for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv & |.Sv.| c= [#] Sv holds
BCS n,Sv is SubSimplicialComplex of BCS n,Kv
let S be non void SubSimplicialComplex of Kv; :: thesis: ( |.Kv.| c= [#] Kv & |.S.| c= [#] S implies BCS n,S is SubSimplicialComplex of BCS n,Kv )
assume ( |.Kv.| c= [#] Kv & |.S.| c= [#] S ) ; :: thesis: BCS n,S is SubSimplicialComplex of BCS n,Kv
then ( BCS n,S = subdivision n,(center_of_mass V),S & BCS n,Kv = subdivision n,(center_of_mass V),Kv ) by Def6;
hence BCS n,S is SubSimplicialComplex of BCS n,Kv by SIMPLEX0:65; :: thesis: verum