let X, Y, Z be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision (P | Y),KX is SubSimplicialComplex of subdivision (P | Z),KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st Y c= Z holds
subdivision (P | Y),KX is SubSimplicialComplex of subdivision (P | Z),KX
let P be Function; :: thesis: ( Y c= Z implies subdivision (P | Y),KX is SubSimplicialComplex of subdivision (P | Z),KX )
set PY = subdivision (P | Y),KX;
set PZ = subdivision (P | Z),KX;
A1: dom (P | Z) = Z /\ (dom P) by RELAT_1:90;
assume A2: Y c= Z ; :: thesis: subdivision (P | Y),KX is SubSimplicialComplex of subdivision (P | Z),KX
then Y /\ Z = Y by XBOOLE_1:28;
then A3: dom (P | Y) = (Z /\ Y) /\ (dom P) by RELAT_1:90
.= Y /\ (dom (P | Z)) by A1, XBOOLE_1:16 ;
A4: [#] (subdivision (P | Y),KX) = [#] KX by Def20;
hence [#] (subdivision (P | Y),KX) c= [#] (subdivision (P | Z),KX) by Def20; :: according to SIMPLEX0:def 13 :: thesis: the topology of (subdivision (P | Y),KX) c= the topology of (subdivision (P | Z),KX)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision (P | Y),KX) or x in the topology of (subdivision (P | Z),KX) )
assume x in the topology of (subdivision (P | Y),KX) ; :: thesis: x in the topology of (subdivision (P | Z),KX)
then reconsider A = x as Simplex of (subdivision (P | Y),KX) by PRE_TOPC:def 5;
[#] (subdivision (P | Z),KX) = [#] KX by Def20;
then reconsider B = A as Subset of (subdivision (P | Z),KX) by A4;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A5: A = (P | Y) .: S by Def20;
S /\ Y c= S by XBOOLE_1:17;
then reconsider SY = S /\ Y as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:18;
A6: ( dom (P | Y) c= Y & (dom (P | Y)) /\ S c= dom (P | Y) ) by RELAT_1:87, XBOOLE_1:17;
then A7: (dom (P | Y)) /\ S c= Y by XBOOLE_1:1;
B = (P | Y) .: ((dom (P | Y)) /\ S) by A5, RELAT_1:145
.= P .: ((dom (P | Y)) /\ S) by A6, RELAT_1:162, XBOOLE_1:1
.= (P | Z) .: ((dom (P | Y)) /\ S) by A2, A7, RELAT_1:162, XBOOLE_1:1
.= (P | Z) .: ((dom (P | Z)) /\ SY) by A3, XBOOLE_1:16
.= (P | Z) .: SY by RELAT_1:145 ;
then B is simplex-like by Def20;
hence x in the topology of (subdivision (P | Z),KX) by PRE_TOPC:def 5; :: thesis: verum