noncomputable def GaloisCorrespondence.goal_160_fundamental_theorem (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] : IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈ