theorem :: FIELD_6:68

for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) is F -finite )