theorem :: FIELD_6:38

for F being strict Field
for E being FieldExtension of F
for T being Subset of E holds
( FAdj (F,T) = F iff T is Subset of F )