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