∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (P : IntermediateField F E → Prop),
  P ⊥ →
    (∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) →
      ∀ (K : IntermediateField F E), K.FG → P K