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 5;
[#] (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:79;
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 5;
the topology of SX c= the topology of KX by Def13;
hence C is simplex-like by A5, PRE_TOPC:def 5; :: thesis: verum

end;

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