theorem lift4: :: FIELD_12:44

for F1, F2 being Field
for E being AlgebraicClosure of F1 st F1 == F2 holds
E is AlgebraicClosure of F2