theorem helpa: :: FIELD_13:32
for R being Ring
for S being RingExtension of R
for T being Subset of S holds
( RAdj (R,T) == R iff T is Subset of R )