theorem :: SIMPLEX0:15

for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered ) by Lm2;