for R, S being Ring holds
( R == S iff ex f being Function of R,S st
( f = id R & f is isomorphism ) )