let K be SimplicialComplexStr; :: thesis: ( not K is void & K is subset-closed implies not K is with_non-empty_elements )
assume A1: ( not K is void & K is subset-closed ) ; :: thesis: not K is with_non-empty_elements
then ex x being set st x in the_family_of K by XBOOLE_0:def 1;
hence not K is with_non-empty_elements by A1, Def8; :: thesis: verum