theorem :: FIELD_7:39

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F st K is E -algebraic & E is F -algebraic holds
K is F -algebraic