theorem :: FIELD_12:29

for F being Field ex E being Field st E is AlgebraicClosure of F