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

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