let K be SimplicialComplexStr; :: thesis: ( not K is with_non-empty_elements implies not K is void )
assume not K is with_non-empty_elements ; :: thesis: not K is void
then the topology of K is with_empty_element by Def8;
hence not K is void by PENCIL_1:def 4; :: thesis: verum