∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2], FiniteDimensional K ↥(E1 ⊔ E2)