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: K is empty-membered
assume not K is empty-membered ; :: thesis: contradiction
then not the topology of K is empty-membered by Def7;
then consider D being non empty set such that
A2: D in the topology of K by SETFAM_1:def 11;
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, PRE_TOPC:def 5;
then v is vertex-like by Def3;
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 set such that
A4: x in Vertices K by XBOOLE_0:def 1;
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 by Def3;
S in the topology of K by A5, PRE_TOPC:def 5;
then not the topology of K is empty-membered by A6, SETFAM_1:def 11;
hence contradiction by A3, Def7; :: thesis: verum