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

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