let n be Nat; 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; 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; 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; ( |.Kv.| c= [#] Kv & |.S.| c= [#] S implies BCS (n,S) is SubSimplicialComplex of BCS (n,Kv) )
assume
( |.Kv.| c= [#] Kv & |.S.| c= [#] S )
; 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; verum