∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s t : Set M}, s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (s - t) = sSup s - sInf t