let S, T be non empty TopStruct ; :: thesis: ( S,T are_homeomorphic implies T,S are_homeomorphic )
assume S,T are_homeomorphic ; :: thesis: T,S are_homeomorphic
then consider f being Function of S,T such that
A1: f is being_homeomorphism ;
f " is being_homeomorphism by A1, TOPS_2:56;
hence T,S are_homeomorphic ; :: thesis: verum