∀ (K : Type u_2) [inst : Field K] [inst_1 : CharZero K] [Algebra.IsIntegral ℚ K] [NumberField.IsTotallyComplex K]
  (E : Subfield K) [NumberField.IsTotallyReal ↥E] [Algebra.IsQuadraticExtension (↥E) K],
  E = NumberField.maximalRealSubfield K