∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K), (I ⊓ J) * (I ⊔ J) = I * J