∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : DistribLattice α]
  [inst_3 : OrderBot α] {f : ι → α} {i : ι} {x : α}, Disjoint ((partialSups f) i) x = ∀ j ≤ i, Disjoint (f j) x