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 )

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

( |.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 A3:
Kr is empty-membered
; :: thesis: |.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 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

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