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

assume S,T are_homeomorphic ; :: thesis: R94(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 R94(T,S) by T_0TOPSP:def 1; :: thesis: verum

assume S,T are_homeomorphic ; :: thesis: R94(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 R94(T,S) by T_0TOPSP:def 1; :: thesis: verum