∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (L : IntermediateField.Lifts F E K),
  ∃ (h : { carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(IntermediateField.botEquiv F E) }.carrier ≤ L.carrier),
    ∀ (x : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(IntermediateField.botEquiv F E) }.carrier),
      L.emb ((IntermediateField.inclusion h) x) =
        { carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(IntermediateField.botEquiv F E) }.emb x