:: deftheorem Def7 defines empty-membered SIMPLEX0:def 7 :
for K being SimplicialComplexStr holds
( K is empty-membered iff the topology of K is empty-membered );