let K be SimplicialComplexStr; :: thesis: ( K is with_empty_element implies not K is void )
assume K is with_empty_element ; :: 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