theorem RE1: :: FIELD_6:14

for S being Ring
for R1, R2 being strict Subring of S holds
( R1 = R2 iff the carrier of R1 = the carrier of R2 )