theorem mi1: :: FIELD_12:6

for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds
( ex E being FieldExtension of F ex a being b₁ -algebraic Element of E st p = MinPoly (a,F) iff ( p is monic & p is irreducible ) )