theorem Th25: :: SIMPLEX0:25

for i being Integer
for K being SimplicialComplexStr st ( not K is void or i >= - 1 ) holds
( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )