:: deftheorem defAC defines AlgebraicClosure FIELD_12:def 11 :
for F being Field
for b₂ being FieldExtension of F holds
( b₂ is AlgebraicClosure of F iff ( b₂ is F -algebraic & b₂ is algebraic-closed ) );