let K be SimplicialComplexStr; :: thesis: ( Vertices K is empty iff K is empty-membered )

hereby :: thesis: ( K is empty-membered implies Vertices K is empty )

assume A1: Vertices K is empty ; :: thesis: not K is with_non-empty_element
assume K is with_non-empty_element ; :: thesis: contradiction
then the topology of K is with_non-empty_element ;
then consider D being non empty set such that
A2: D in the topology of K ;
reconsider S = D as Subset of K by A2;
the Element of D in S ;
then reconsider v = the Element of D as Element of K ;
S is simplex-like by A2;
then v is vertex-like ;
hence contradiction by A1, Def4; :: thesis: verum

end;

assume A3: K is empty-membered ; :: thesis: Vertices K is empty
assume not Vertices K is empty ; :: thesis: contradiction
then consider x being object such that
A4: x in Vertices K ;
reconsider x = x as Element of K by A4;
x is vertex-like by A4, Def4;
then consider S being Subset of K such that
A5: S is simplex-like and
A6: x in S ;
S in the topology of K by A5;
then the topology of K is with_non-empty_element by A6;
hence contradiction by A3; :: thesis: verum