for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)