theorem :: RING_4:46

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