let X, Y be non empty TopStruct ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #)
let f be Function of X,Y; :: thesis: for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #)
let g be Function of Y,X; :: thesis: ( f = id X & g = id X & f is continuous & g is continuous implies TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #) )
assume that
A1: f = id X and
A2: g = id X and
A3: f is continuous and
A4: g is continuous ; :: thesis: TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #)
A5: ( [#] X <> {} & [#] Y <> {} ) ;
A6: the carrier of X = dom f by FUNCT_2:def 1
.= the carrier of Y by A1, A2, FUNCT_2:def 1 ;
the topology of X = the topology of Y

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the topology of Y c= the topology of X

let A be set ; :: thesis: ( A in the topology of X implies A in the topology of Y )
assume A7: A in the topology of X ; :: thesis: A in the topology of Y
then reconsider B = A as Subset of X ;
B is open by A7, PRE_TOPC:def 5;
then A8: g " B is open by A4, A5, TOPS_2:55;
g " B = B by A2, FUNCT_2:171;
hence A in the topology of Y by A8, PRE_TOPC:def 5; :: thesis: verum

end;

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of Y or A in the topology of X )
assume A9: A in the topology of Y ; :: thesis: A in the topology of X
then reconsider B = A as Subset of Y ;
B is open by A9, PRE_TOPC:def 5;
then A10: f " B is open by A3, A5, TOPS_2:55;
f " B = B by A1, A6, FUNCT_2:171;
hence A in the topology of X by A10, PRE_TOPC:def 5; :: thesis: verum

end;

hence TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #) by A6; :: thesis: verum