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