theorem :: FIELD_7:37

for F being Field
for E being FieldExtension of F holds
( E is F -finite iff ex T being finite b₁ -algebraic Subset of E st E == FAdj (F,T) )