let S, T be TopStruct ; :: thesis: ( R91(S,T) implies R91(T,S) )
assume S,T are_homeomorphic ; :: thesis: R91(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 R91(T,S) by T_0TOPSP:def 1; :: thesis: verum