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