let RLS be non empty RLSStruct ; :: thesis:
let Kr be SimplicialComplexStr of RLS; :: thesis:
set TOP = the topology of Kr;
set C = Complex_of the topology of Kr;
( [#] (Complex_of the topology of Kr) = [#] Kr & [#] Kr c= the carrier of RLS ) by SIMPLEX0:def 9;
then reconsider C = Complex_of the topology of Kr as SimplicialComplexStr of RLS by SIMPLEX0:def 9;
A1: |.Kr.| c= |.C.|

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in |.Kr.| ; :: thesis:
then consider A being Subset of Kr such that
A2: A is simplex-like and
A3: x in conv (@ A) by Def3;
reconsider B = A as Subset of C ;
A in the topology of Kr by A2;
then A in the topology of C by SIMPLEX0:2;
then A4: B is simplex-like ;
@ A = @ B ;
hence x in |.C.| by A3, A4, Def3; :: thesis:

end;

for A being Subset of C st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) )

let A be Subset of C; :: thesis:
assume A is simplex-like ; :: thesis:
then A in the topology of C ;
then consider B being set such that
A5: A c= B and
A6: B in the topology of Kr by SIMPLEX0:2;
reconsider B = B as Subset of Kr by A6;
take B ; :: thesis:
thus ( B is simplex-like & conv (@ A) c= conv (@ B) ) by A5, A6, RLAFFIN1:3; :: thesis:

end;