theorem :: FIELD_6:34

for F being Field
for R being RingExtension of F
for T being Subset of R holds F is Subfield of RAdj (F,T)