:: deftheorem Def1 defines -extending FIELD_4:def 1 :
for R, S being Ring holds
( S is R -extending iff R is Subring of S );