let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS
for P being SubdivisionStr of Kr holds |.Kr.| = |.P.|
let Kr be SimplicialComplexStr of RLS; :: thesis: for P being SubdivisionStr of Kr holds |.Kr.| = |.P.|
let P be SubdivisionStr of Kr; :: thesis: |.Kr.| = |.P.|
thus |.Kr.| c= |.P.| by Def4; :: according to XBOOLE_0:def 10 :: thesis: |.P.| c= |.Kr.|
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.P.| or x in |.Kr.| )
assume x in |.P.| ; :: thesis: x in |.Kr.|
then consider A being Subset of P such that
A1: A is simplex-like and
A2: x in conv (@ A) by Def3;
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) by A1, Def4;
hence x in |.Kr.| by A2, Def3; :: thesis: verum