let X, Y be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision (Y | P),KX = subdivision P,KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st P .: the topology of KX c= Y holds
subdivision (Y | P),KX = subdivision P,KX
let P be Function; :: thesis: ( P .: the topology of KX c= Y implies subdivision (Y | P),KX = subdivision P,KX )
set PK = subdivision P,KX;
( P = (rng P) | P & Y | ((rng P) | P) = (Y /\ (rng P)) | P ) by RELAT_1:126, RELAT_1:127;
then reconsider PY = subdivision (Y | P),KX as SubSimplicialComplex of subdivision P,KX by Th56, XBOOLE_1:17;
A1: ( [#] PY = [#] KX & [#] (subdivision P,KX) = [#] KX ) by Def20;
assume A2: P .: the topology of KX c= Y ; :: thesis: subdivision (Y | P),KX = subdivision P,KX
A3: the topology of (subdivision P,KX) c= the topology of PY

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision P,KX) or x in the topology of PY )
assume x in the topology of (subdivision P,KX) ; :: thesis: x in the topology of PY
then reconsider A = x as Simplex of (subdivision P,KX) by PRE_TOPC:def 5;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: A = P .: S by Def20;
reconsider A = A as Subset of PY by A1;
S c= the topology of KX

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in S or y in the topology of KX )
assume A5: y in S ; :: thesis: y in the topology of KX
reconsider y = y as Subset of KX by A5;
y is simplex-like by A5, TOPS_2:def 1;
hence y in the topology of KX by PRE_TOPC:def 5; :: thesis: verum

end;

then A c= P .: the topology of KX by A4, RELAT_1:156;
then A /\ Y = A by A2, XBOOLE_1:1, XBOOLE_1:28;
then A = (Y | P) .: S by A4, FUNCT_1:126;
then A is simplex-like by Def20;
hence x in the topology of PY by PRE_TOPC:def 5; :: thesis: verum

end;

the topology of PY c= the topology of (subdivision P,KX) by Def13;
hence subdivision (Y | P),KX = subdivision P,KX by A1, A3, XBOOLE_0:def 10; :: thesis: verum