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 not A is dependent holds
ex B being Subset of Kr st
( not B is dependent & conv (@ A) c= conv (@ B) )
let A2 be Subset of P2; :: thesis: ( not A2 is dependent implies ex B being Subset of Kr st
( not B is dependent & conv (@ A2) c= conv (@ B) ) )
assume not A2 is dependent ; :: thesis: ex B being Subset of Kr st
( not B is dependent & conv (@ A2) c= conv (@ B) )
then consider A1 being Subset of P1 such that
A1: not A1 is dependent and
A2: conv (@ A2) c= conv (@ A1) by Def4;
ex A being Subset of Kr st
( not A is dependent & conv (@ A1) c= conv (@ A) ) by A1, Def4;
hence ex B being Subset of Kr st
( not B is dependent & conv (@ A2) c= conv (@ B) ) by A2, XBOOLE_1:1; :: thesis: verum