let RLS be non empty RLSStruct ; :: thesis: for A being Subset of RLS holds |.(Complex_of {A}).| = conv A
let A be Subset of RLS; :: thesis: |.(Complex_of {A}).| = conv A
set C = Complex_of {A};
reconsider A1 = A as Subset of (Complex_of {A}) ;
A1: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: conv A c= |.(Complex_of {A}).|

let x be object ; :: thesis: ( x in |.(Complex_of {A}).| implies x in conv A )
assume x in |.(Complex_of {A}).| ; :: thesis: x in conv A
then consider S being Subset of (Complex_of {A}) such that
A2: S is simplex-like and
A3: x in conv (@ S) by Def3;
S in the topology of (Complex_of {A}) by A2;
then conv (@ S) c= conv A by A1, RLAFFIN1:3;
hence x in conv A by A3; :: thesis: verum

end;

A c= A ;
then ( @ A1 = A & A1 is simplex-like ) by A1;
hence conv A c= |.(Complex_of {A}).| by Th5; :: thesis: verum