theorem XX: :: FIELD_12:30

for F being Field
for E being b₁ -algebraic FieldExtension of F ex A being AlgebraicClosure of F st E is Subfield of A