theorem lemA: :: FIELD_12:9

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