:: deftheorem defred defines @ FIELD_7:def 6 :
for R being Ring
for S being RingExtension of R
for a being Element of S st a is R -membered holds
@ (R,a) = a;