for K being non void subset-closed SimplicialComplexStr
for S being finite Simplex of K holds S is Simplex of (card S) - 1,K