theorem Th20: :: SIMPLEX1:20

for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS ((n + 1),Kv) = BCS (BCS (n,Kv))