let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let SX be SubSimplicialComplex of KX; :: thesis: for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let P be Function; :: thesis: subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
set PS = subdivision (P,SX);
set PK = subdivision (P,KX);
A1: [#] SX c= [#] KX by Def13;
A2: [#] (subdivision (P,KX)) = [#] KX by Def20;
hence [#] (subdivision (P,SX)) c= [#] (subdivision (P,KX)) by A1, Def20; :: according to SIMPLEX0:def 13 :: thesis: the topology of (subdivision (P,SX)) c= the topology of (subdivision (P,KX))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision (P,SX)) or x in the topology of (subdivision (P,KX)) )
assume x in the topology of (subdivision (P,SX)) ; :: thesis: x in the topology of (subdivision (P,KX))
then reconsider A = x as Simplex of (subdivision (P,SX)) by PRE_TOPC:def 2;
[#] (subdivision (P,SX)) = [#] SX by Def20;
then reconsider B = A as Subset of (subdivision (P,KX)) by A1, A2, XBOOLE_1:1;
consider SS being c=-linear finite simplex-like Subset-Family of SX such that
A3: A = P .: SS by Def20;
bool ([#] SX) c= bool ([#] KX) by A1, ZFMISC_1:67;
then reconsider SK = SS as c=-linear finite Subset-Family of KX by XBOOLE_1:1;
SK is simplex-like

proof

let C be Subset of KX; :: according to TOPS_2:def 1 :: thesis: ( not C in SK or C is simplex-like )
assume A4: C in SK ; :: thesis: C is simplex-like
then reconsider c = C as Subset of SX ;
c is simplex-like by A4, TOPS_2:def 1;
then A5: c in the topology of SX by PRE_TOPC:def 2;
the topology of SX c= the topology of KX by Def13;
hence C is simplex-like by A5, PRE_TOPC:def 2; :: thesis: verum

end;

then B is simplex-like by A3, Def20;
hence x in the topology of (subdivision (P,KX)) by PRE_TOPC:def 2; :: thesis: verum