∀ (R : Type u_2) (A : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [NoZeroDivisors A]
  (I B : Set A),
  AlgebraicIndepOn R id I →
    ¬Maximal (AlgebraicIndepOn R id) I →
      Maximal (AlgebraicIndepOn R id) B → ∃ x ∈ B \ I, AlgebraicIndepOn R id (insert x I)