let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS
for P1 being SubdivisionStr of Kr
for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr
let Kr be SimplicialComplexStr of RLS; :: thesis: for P1 being SubdivisionStr of Kr
for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr
let P1 be SubdivisionStr of Kr; :: thesis: for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr
let P2 be SubdivisionStr of P1; :: thesis: P2 is SubdivisionStr of Kr
|.P2.| = |.P1.| by Th10
.= |.Kr.| by Th10 ;
hence |.Kr.| c= |.P2.| ; :: according to SIMPLEX1:def 4 :: thesis: for A being Subset of P2 st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) )
let A2 be Subset of P2; :: thesis: ( A2 is simplex-like implies ex B being Subset of Kr st
( B is simplex-like & conv (@ A2) c= conv (@ B) ) )
assume A2 is simplex-like ; :: thesis: ex B being Subset of Kr st
( B is simplex-like & conv (@ A2) c= conv (@ B) )
then consider A1 being Subset of P1 such that
A1: A1 is simplex-like and
A2: conv (@ A2) c= conv (@ A1) by Def4;
ex A being Subset of Kr st
( A is simplex-like & conv (@ A1) c= conv (@ A) ) by A1, Def4;
hence ex B being Subset of Kr st
( B is simplex-like & conv (@ A2) c= conv (@ B) ) by A2, XBOOLE_1:1; :: thesis: verum