theorem :: FIELD_13:54

for F being Field
for E being b₁ -algebraic FieldExtension of F holds
( E is F -normal iff for a being Element of E holds MinPoly (a,F) splits_in E ) by lemmin;