∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L)
  {K' : LieSubalgebra R L} (h : K ≤ K'),
  (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K