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