theorem :: FIELD_7:40

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