let X, Y, Z be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((Y | P),KX) is SubSimplicialComplex of subdivision ((Z | P),KX)
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st Y c= Z holds
subdivision ((Y | P),KX) is SubSimplicialComplex of subdivision ((Z | P),KX)
let P be Function; :: thesis: ( Y c= Z implies subdivision ((Y | P),KX) is SubSimplicialComplex of subdivision ((Z | P),KX) )
assume A1: Y c= Z ; :: thesis: subdivision ((Y | P),KX) is SubSimplicialComplex of subdivision ((Z | P),KX)
set PZ = subdivision ((Z | P),KX);
set PY = subdivision ((Y | P),KX);
A2: [#] (subdivision ((Y | P),KX)) = [#] KX by Def20;
hence [#] (subdivision ((Y | P),KX)) c= [#] (subdivision ((Z | P),KX)) by Def20; :: according to SIMPLEX0:def 13 :: thesis: the topology of (subdivision ((Y | P),KX)) c= the topology of (subdivision ((Z | P),KX))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision ((Y | P),KX)) or x in the topology of (subdivision ((Z | P),KX)) )
assume x in the topology of (subdivision ((Y | P),KX)) ; :: thesis: x in the topology of (subdivision ((Z | P),KX))
then reconsider A = x as Simplex of (subdivision ((Y | P),KX)) by PRE_TOPC:def 2;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A3: A = (Y | P) .: S by Def20;
S /\ (dom (Y | P)) c= S by XBOOLE_1:17;
then reconsider Sd = S /\ (dom (Y | P)) as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:11;
Y | (Z | P) = Y | P by A1, RELAT_1:99;
then A4: (Y | P) .: Sd c= (Z | P) .: Sd by RELAT_1:86, RELAT_1:124;
[#] (subdivision ((Z | P),KX)) = [#] KX by Def20;
then reconsider A = A as Subset of (subdivision ((Z | P),KX)) by A2;
A5: (Z | P) .: Sd c= (Y | P) .: Sd

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Z | P) .: Sd or y in (Y | P) .: Sd )
assume y in (Z | P) .: Sd ; :: thesis: y in (Y | P) .: Sd
then consider x being set such that
A6: x in dom (Z | P) and
A7: x in Sd and
A8: (Z | P) . x = y by FUNCT_1:def 6;
A9: x in dom (Y | P) by A7, XBOOLE_0:def 4;
P . x = y by A6, A8, FUNCT_1:53;
then (Y | P) . x = y by A9, FUNCT_1:53;
hence y in (Y | P) .: Sd by A7, A9, FUNCT_1:def 6; :: thesis: verum

end;

A = (Y | P) .: Sd by A3, RELAT_1:112;
then A = (Z | P) .: Sd by A4, A5, XBOOLE_0:def 10;
then A is simplex-like by Def20;
hence x in the topology of (subdivision ((Z | P),KX)) by PRE_TOPC:def 2; :: thesis: verum