theorem :: FIELD_13:28

for R1, R2 being Ring st R1 == R2 holds
R2 == R1 ;