theorem :: SIMPLEX1:19

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.| by Th10;