theorem RAt: :: FIELD_6:30

for R being Ring
for S being RingExtension of R
for T being Subset of S holds T is Subset of (RAdj (R,T))