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