theorem :: FIELD_13:29

for R1, R2, R3 being Ring st R1 == R2 & R2 == R3 holds
R1 == R3 by helpb;