theorem FAsub: :: FIELD_6:36

for F being Field
for E being FieldExtension of F
for T being Subset of E holds F is Subfield of FAdj (F,T)