:: deftheorem defines carrierRA FIELD_6:def 3 :
for R being Ring
for S being RingExtension of R
for T being Subset of S holds carrierRA T = { x where x is Element of S : for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U } ;