theorem :: FIELD_14:76

for F being infinite Field
for E being b₁ -finite FieldExtension of F holds
( E is F -simple iff IntermediateFields (E,F) is finite )