theorem :: MATGRP_0:2

for R1, R2 being Ring st R1,R2 are_isomorphic holds
( R2 is R1 -isomorphic & R1 is R2 -isomorphic )