let R be domRing; :: thesis: R is domRingExtension of R
R is Subring of R by Th1;
hence R is domRingExtension of R by Def1; :: thesis: verum