for D being non empty set
for K being non void subset-closed SimplicialComplexStr of D
for S being non void SubSimplicialComplex of K
for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K