for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds degree SX <= degree KX