:: deftheorem Def4 defines SubdivisionStr SIMPLEX1:def 4 :
for RLS being non empty RLSStruct
for Kr, b₃ being SimplicialComplexStr of RLS holds
( b₃ is SubdivisionStr of Kr iff ( |.Kr.| c= |.b₃.| & ( for A being Subset of b₃ st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ) ) );