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

( 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