let K be SimplicialComplexStr; :: thesis: ( not K is void & K is empty-membered implies not K is with_non-empty_elements )
assume ( not K is void & K is empty-membered ) ; :: thesis: not K is with_non-empty_elements
then the topology of K is with_empty_element by Def7;
hence not K is with_non-empty_elements by Def8; :: thesis: verum