theorem lift3a: :: FIELD_12:33

for F being Field
for A1, A2 being AlgebraicClosure of F st A1 is A2 -extending holds
A2 == A1