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;

then ( @ A1 = A & A1 is simplex-like ) by A1;

hence conv A c= |.(Complex_of {A}).| by Th5; :: thesis: verum

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}).|

A c= 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;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

then ( @ A1 = A & A1 is simplex-like ) by A1;

hence conv A c= |.(Complex_of {A}).| by Th5; :: thesis: verum