theorem Th23: :: SIMPLEX1:23

for n being 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)