theorem Th30: :: SIMPLEX1:30

for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ) holds
degree Kv = degree (BCS Kv)