theorem :: FIELD_12:21

for F being Field holds
( F is algebraic-closed iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ) by al1;