let RLS be non empty RLSStruct ; :: thesis: for K1r, K2r being SimplicialComplexStr of RLS st the topology of K1r c= the topology of K2r holds

|.K1r.| c= |.K2r.|

let K1r, K2r be SimplicialComplexStr of RLS; :: thesis: ( the topology of K1r c= the topology of K2r implies |.K1r.| c= |.K2r.| )

assume A1: the topology of K1r c= the topology of K2r ; :: thesis: |.K1r.| c= |.K2r.|

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.K1r.| or x in |.K2r.| )

assume x in |.K1r.| ; :: thesis: x in |.K2r.|

then consider A being Subset of K1r such that

A2: A is simplex-like and

A3: x in conv (@ A) by Def3;

A4: A in the topology of K1r by A2;

then A in the topology of K2r by A1;

then reconsider A1 = A as Subset of K2r ;

( @ A = @ A1 & A1 is simplex-like ) by A1, A4;

hence x in |.K2r.| by A3, Def3; :: thesis: verum

|.K1r.| c= |.K2r.|

let K1r, K2r be SimplicialComplexStr of RLS; :: thesis: ( the topology of K1r c= the topology of K2r implies |.K1r.| c= |.K2r.| )

assume A1: the topology of K1r c= the topology of K2r ; :: thesis: |.K1r.| c= |.K2r.|

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.K1r.| or x in |.K2r.| )

assume x in |.K1r.| ; :: thesis: x in |.K2r.|

then consider A being Subset of K1r such that

A2: A is simplex-like and

A3: x in conv (@ A) by Def3;

A4: A in the topology of K1r by A2;

then A in the topology of K2r by A1;

then reconsider A1 = A as Subset of K2r ;

( @ A = @ A1 & A1 is simplex-like ) by A1, A4;

hence x in |.K2r.| by A3, Def3; :: thesis: verum