:: deftheorem Def18 defines Simplex SIMPLEX0:def 18 :
for K being non void subset-closed SimplicialComplexStr
for i being Real st i is integer holds
for b₃ being finite Simplex of K holds
( ( - 1 <= i & i <= degree K implies ( b₃ is Simplex of i,K iff card b₃ = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b₃ is Simplex of i,K iff b₃ is empty ) ) );