:: deftheorem Def8 defines with_non-empty_elements SIMPLEX0:def 8 :
for K being SimplicialComplexStr holds
( K is with_non-empty_elements iff the topology of K is with_non-empty_elements );