theorem ClA: :: FIELD_12:25

for F being Field holds
( F is algebraic-closed iff for E being b₁ -algebraic FieldExtension of F holds E == F )