let S, T be TopStruct ; :: thesis: ( R93(S,T) implies R93(T,S) )

assume S,T are_homeomorphic ; :: thesis: R93(T,S)

then consider f being Function of S,T such that

A1: f is being_homeomorphism by T_0TOPSP:def 1;

f " is being_homeomorphism by A1, Th3;

hence R93(T,S) by T_0TOPSP:def 1; :: thesis: verum

assume S,T are_homeomorphic ; :: thesis: R93(T,S)

then consider f being Function of S,T such that

A1: f is being_homeomorphism by T_0TOPSP:def 1;

f " is being_homeomorphism by A1, Th3;

hence R93(T,S) by T_0TOPSP:def 1; :: thesis: verum