:: deftheorem defmem defines -membered FIELD_7:def 5 :
for R being Ring
for S being RingExtension of R
for a being Element of S holds
( a is R -membered iff a in the carrier of R );