let F be Field; :: thesis: for A1, A2 being AlgebraicClosure of F st A1 is A2 -extending holds
A2 == A1
let E1, E2 be AlgebraicClosure of F; :: thesis: ( E1 is E2 -extending implies E2 == E1 )
assume E1 is E2 -extending ; :: thesis: E2 == E1
then reconsider K = E1 as E2 -extending FieldExtension of F ;
K is E2 -algebraic by FIELD_7:40;
hence E2 == E1 by ClA; :: thesis: verum