theorem :: FIELD_4:5

for R being domRing holds R is domRingExtension of R