:: deftheorem defines @ FIELD_9:def 1 :
for R being Ring
for S being RingExtension of R
for a being b₁ -membered Element of S holds @ a = a;