let R be comRing; :: thesis: R is comRingExtension of R
R is Subring of R by Th1;
hence R is comRingExtension of R by Def1; :: thesis: verum