let T1, T2 be TopSpace; :: thesis: ( ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) implies TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #) )
assume A1: for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ; :: thesis: TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #)
the topology of T1 = the topology of T2

proof

thus the topology of T1 c= the topology of T2 by A1, Lm2; :: according to XBOOLE_0:def 10 :: thesis: the topology of T2 c= the topology of T1
thus the topology of T2 c= the topology of T1 by A1, Lm2; :: thesis: verum

end;

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