∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instSub = { sub := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 - x2) ↑s ↑t, lower' := ⋯ } }