theorem main1: :: FIELD_12:28

for F being Field ex E being FieldExtension of F st E is algebraic-closed