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 5;
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:18;
Y | (Z | P) = Y | P by A1, RELAT_1:130;
then A4: (Y | P) .: Sd c= (Z | P) .: Sd by RELAT_1:117, RELAT_1:157;
[#] (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 12;
A9: x in dom (Y | P) by A7, XBOOLE_0:def 4;
P . x = y by A6, A8, FUNCT_1:85;
then (Y | P) . x = y by A9, FUNCT_1:85;
hence y in (Y | P) .: Sd by A7, A9, FUNCT_1:def 12; :: thesis: verum

end;

A = (Y | P) .: Sd by A3, RELAT_1:145;
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 5; :: thesis: verum