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 5;
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 5; :: 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 5;
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 5; :: thesis: verum

end;

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