let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS holds
( |.Kr.| is empty iff Kr is empty-membered )
let Kr be SimplicialComplexStr of RLS; :: thesis: ( |.Kr.| is empty iff Kr is empty-membered )

hereby :: thesis: ( Kr is empty-membered implies |.Kr.| is empty )

assume A1: |.Kr.| is empty ; :: thesis: not Kr is with_non-empty_element
assume Kr is with_non-empty_element ; :: thesis: contradiction
then the topology of Kr is with_non-empty_element ;
then consider x being non empty set such that
A2: x in the topology of Kr ;
reconsider X = x as Subset of Kr by A2;
( ex y being object st y in conv (@ X) & X is simplex-like ) by A2, XBOOLE_0:def 1;
hence contradiction by A1, Def3; :: thesis: verum

end;

assume A3: Kr is empty-membered ; :: thesis: |.Kr.| is empty
assume not |.Kr.| is empty ; :: thesis: contradiction
then consider x being object such that
A4: x in |.Kr.| ;
consider A being Subset of Kr such that
A5: ( A is simplex-like & x in conv (@ A) ) by A4, Def3;
( not A is empty & A in the topology of Kr ) by A5;
then the topology of Kr is with_non-empty_element ;
hence contradiction by A3; :: thesis: verum