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 not A is dependent holds
ex B being Subset of Kr st
( not B is dependent & conv (@ A) c= conv (@ B) )
thus for A being Subset of Kr st not A is dependent holds
ex B being Subset of Kr st
( not B is dependent & conv (@ A) c= conv (@ B) ) ; :: thesis: verum