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:61;
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:61
.= 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 object ; :: 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 2;
[#] (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:11;
A6: ( dom (P | Y) c= Y & (dom (P | Y)) /\ S c= dom (P | Y) ) by RELAT_1:58, XBOOLE_1:17;
then A7: (dom (P | Y)) /\ S c= Y ;
B = (P | Y) .: ((dom (P | Y)) /\ S) by A5, RELAT_1:112
.= P .: ((dom (P | Y)) /\ S) by A6, RELAT_1:129, XBOOLE_1:1
.= (P | Z) .: ((dom (P | Y)) /\ S) by A2, A7, RELAT_1:129, XBOOLE_1:1
.= (P | Z) .: ((dom (P | Z)) /\ SY) by A3, XBOOLE_1:16
.= (P | Z) .: SY by RELAT_1:112 ;
then B is simplex-like by Def20;
hence x in the topology of (subdivision ((P | Z),KX)) ; :: thesis: verum