let T be S -isomorphic Ring; :: thesis: T is R -isomorphic
the Isomorphism of S,T * the Isomorphism of R,S is onto by FUNCT_2:27;
hence T is R -isomorphic ; :: thesis: verum