let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS holds Complex_of the topology of Kr is SubdivisionStr of Kr
let Kr be SimplicialComplexStr of RLS; :: thesis: Complex_of the topology of Kr is SubdivisionStr of Kr
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.|
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.Kr.| or x in |.C.| )
assume x in |.Kr.| ; :: thesis: x in |.C.|
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: verum
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) )
proof
let A be Subset of C; :: thesis: ( A is simplex-like implies ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) )

assume A is simplex-like ; :: thesis: ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) )

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: ( B is simplex-like & conv (@ A) c= conv (@ B) )
thus ( B is simplex-like & conv (@ A) c= conv (@ B) ) by ; :: thesis: verum
end;
hence Complex_of the topology of Kr is SubdivisionStr of Kr by ; :: thesis: verum