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