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