theorem Th24: :: SIMPLEX1:24

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