:: deftheorem defines -primitive FIELD_14:def 8 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -primitive iff E == FAdj (F,{a}) );