let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS holds Kr is SubdivisionStr of Kr

let Kr be SimplicialComplexStr of RLS; :: thesis: Kr is SubdivisionStr of Kr

thus |.Kr.| c= |.Kr.| ; :: according to SIMPLEX1:def 4 :: thesis: for A being Subset of Kr st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) )

thus for A being Subset of Kr st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ; :: thesis: verum

let Kr be SimplicialComplexStr of RLS; :: thesis: Kr is SubdivisionStr of Kr

thus |.Kr.| c= |.Kr.| ; :: according to SIMPLEX1:def 4 :: thesis: for A being Subset of Kr st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) )

thus for A being Subset of Kr st A is simplex-like holds

ex B being Subset of Kr st

( B is simplex-like & conv (@ A) c= conv (@ B) ) ; :: thesis: verum