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: Kr is empty-membered
assume not Kr is empty-membered ; :: thesis: contradiction
then not the topology of Kr is empty-membered by SIMPLEX0:def 7;
then consider x being non empty set such that
A2: x in the topology of Kr by SETFAM_1:def 11;
reconsider X = x as Subset of Kr by A2;
( ex y being set st y in conv (@ X) & not X is dependent ) by A2, PRE_TOPC:def 5, 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 set such that
A4: x in |.Kr.| by XBOOLE_0:def 1;
consider A being Subset of Kr such that
A5: ( not A is dependent & x in conv (@ A) ) by A4, Def3;
( not A is empty & A in the topology of Kr ) by A5, PRE_TOPC:def 5;
then not the topology of Kr is empty-membered by SETFAM_1:def 11;
hence contradiction by A3, SIMPLEX0:def 7; :: thesis: verum