for i being Integer
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of i,K st not S is empty holds
i is natural