let X be set ; :: thesis: for P being Function
for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
let P be Function; :: thesis: for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
let K1, K2 be SimplicialComplexStr of X; :: thesis: ( TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) implies subdivision (P,K1) = subdivision (P,K2) )
assume A1: TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) ; :: thesis: subdivision (P,K1) = subdivision (P,K2)
set P1 = subdivision (P,K1);
set P2 = subdivision (P,K2);
A2: ( [#] K1 = [#] (subdivision (P,K1)) & [#] K2 = [#] (subdivision (P,K2)) ) by Def20;
A3: the topology of (subdivision (P,K1)) c= the topology of (subdivision (P,K2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision (P,K1)) or x in the topology of (subdivision (P,K2)) )
assume A4: x in the topology of (subdivision (P,K1)) ; :: thesis: x in the topology of (subdivision (P,K2))
then reconsider A = x as Subset of (subdivision (P,K1)) ;
reconsider A1 = A as Subset of (subdivision (P,K2)) by A1, A2;
A is simplex-like by A4, PRE_TOPC:def 2;
then consider S being c=-linear finite simplex-like Subset-Family of K1 such that
A5: A = P .: S by Def20;
reconsider S1 = S as Subset-Family of K2 by A1;
S c= the topology of K1 by Th14;
then S1 is simplex-like by A1, Th14;
then A1 is simplex-like by A5, Def20;
hence x in the topology of (subdivision (P,K2)) by PRE_TOPC:def 2; :: thesis: verum

end;

the topology of (subdivision (P,K2)) c= the topology of (subdivision (P,K1))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision (P,K2)) or x in the topology of (subdivision (P,K1)) )
assume A6: x in the topology of (subdivision (P,K2)) ; :: thesis: x in the topology of (subdivision (P,K1))
then reconsider A = x as Subset of (subdivision (P,K2)) ;
reconsider A1 = A as Subset of (subdivision (P,K1)) by A1, A2;
A is simplex-like by A6, PRE_TOPC:def 2;
then consider S being c=-linear finite simplex-like Subset-Family of K2 such that
A7: A = P .: S by Def20;
reconsider S1 = S as Subset-Family of K1 by A1;
S c= the topology of K2 by Th14;
then S1 is simplex-like by A1, Th14;
then A1 is simplex-like by A7, Def20;
hence x in the topology of (subdivision (P,K1)) by PRE_TOPC:def 2; :: thesis: verum

end;

hence subdivision (P,K1) = subdivision (P,K2) by A1, A2, A3, XBOOLE_0:def 10; :: thesis: verum