let T be RingExtension of S; :: thesis: T is R -extending

( S is Subring of T & R is Subring of S ) by Def1;

hence T is R -extending by ALGNUM_1:1; :: thesis: verum

( S is Subring of T & R is Subring of S ) by Def1;

hence T is R -extending by ALGNUM_1:1; :: thesis: verum