Difference of sSups is less than sSup of difference

Stream: Is there code for X?

[Luigi Massacci]

Do we have something like this:

lemma abs_sub_Ssup_le_sSup (α : Type*) (f g : α → ℝ) (hs : BddAbove (Set.range f))
  (ht : BddAbove (Set.range g)) :
  |sSup {f x | x} - sSup {g x | x}| ≤ sSup {|f x - g x| | x}:= by sorry

(Maybe the functions also need to be nonnegative)