theorem ext0: :: FIELD_13:30
for R being Ring
for S being RingExtension of R
for T1, T2 being Subset of S st T1 c= T2 holds
RAdj (R,T1) is Subring of RAdj (R,T2)