let X1, X2 be TopSpace; :: thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; :: thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not Cl C1 = Cl C2 ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ; :: thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

now :: thesis: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )

let C1 be Subset of X1; :: thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
let C2 be Subset of X2; :: thesis: ( C1 = C2 implies ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) ) )
assume A3: C1 = C2 ; :: thesis: ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
thus ( C1 is closed implies C2 is closed ) :: thesis: ( C2 is closed implies C1 is closed )

proof

assume C1 is closed ; :: thesis: C2 is closed
then C1 = Cl C1 by PRE_TOPC:22;
then C2 = Cl C2 by A2, A3;
hence C2 is closed ; :: thesis: verum

end;

thus ( C2 is closed implies C1 is closed ) :: thesis: verum

proof

assume C2 is closed ; :: thesis: C1 is closed
then C2 = Cl C2 by PRE_TOPC:22;
then C1 = Cl C1 by A2, A3;
hence C1 is closed ; :: thesis: verum

end;

end;

hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th73; :: thesis: verum