:: deftheorem defines Alg_El FIELD_7:def 13 :
for F being Field
for E being FieldExtension of F holds Alg_El E = { a where a is b₁ -algebraic Element of E : verum } ;