theorem :: FIELD_4:3

for R being Ring holds R is RingExtension of R