theorem RAsub: :: FIELD_6:31
for R being Ring
for S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj (R,T)