let K be SimplicialComplexStr; :: thesis: ( not K is empty-membered implies not K is void )
assume not K is empty-membered ; :: thesis: not K is void
then not the topology of K is empty-membered by Def7;
hence not K is void by PENCIL_1:def 4; :: thesis: verum