:: deftheorem defines @ SIMPLEX1:def 1 :
for X being 1-sorted
for K being SimplicialComplexStr of X
for A being Subset of K holds @ A = A;