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