for R being comRing holds R is comRingExtension of R