theorem Th18: :: SIMPLEX1:18

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