∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [inst : LE α] [Nonempty ι] [∀ (i : ι), Nonempty (κ i)]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P) → IsRelUpperSet (⋂ i, ⋂ j, f i j) P