let T1, T2 be TopSpace; :: thesis: ( the carrier of T1 = the carrier of T2 & ( for A1 being Subset of
for A2 being Subset of st A1 = A2 holds
Cl A1 = Cl A2 ) implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: for A1 being Subset of
for A2 being Subset of st A1 = A2 holds
Cl A1 = Cl A2 ; :: thesis: the topology of T1 = the topology of T2

now

let A be set ; :: thesis: ( ( A is closed Subset of implies A is closed Subset of ) & ( A is closed Subset of implies A is closed Subset of ) )
thus ( A is closed Subset of implies A is closed Subset of ) :: thesis: ( A is closed Subset of implies A is closed Subset of )

proof

assume A is closed Subset of ; :: thesis: A is closed Subset of
then reconsider A1 = A as closed Subset of ;
reconsider A2 = A1 as Subset of by A1;
Cl A1 = A1 by PRE_TOPC:52;
then Cl A2 = A2 by A2;
hence A is closed Subset of ; :: thesis: verum

end;

assume A is closed Subset of ; :: thesis: A is closed Subset of
then reconsider A2 = A as closed Subset of ;
reconsider A1 = A2 as Subset of by A1;
Cl A2 = A2 by PRE_TOPC:52;
then Cl A1 = A1 by A2;
hence A is closed Subset of ; :: thesis: verum

end;

then TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #) by Th6;
hence the topology of T1 = the topology of T2 ; :: thesis: verum