theorem :: FIELD_12:23

for F being Field holds
( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F ) by RING_5:70;