let R be Ring; :: thesis: R is RingExtension of R
R is Subring of R by Th1;
hence R is RingExtension of R by Def1; :: thesis: verum