let T1, T2 be TopSpace; :: thesis: ( ( for A being set holds
( A is open Subset of T1 iff A is open 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 open Subset of T1 iff A is open Subset of T2 ) ; :: thesis: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
A2: the topology of T2 c= the topology of T1 by A1, Lm1;
the topology of T1 c= the topology of T2 by A1, Lm1;
then the topology of T1 = the topology of T2 by A2;
hence TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) by A1, Lm1; :: thesis: verum