theorem alg2: :: FIELD_12:20

for F being Field holds
( F is algebraic-closed iff for p being non constant Polynomial of F holds p is with_roots )